Theorem eqrelriiv 5085

Description: Inference from extensionality principle for relations. (Contributed by NM, 17-Mar-1995.)

Hypotheses

Ref	Expression
eqreliiv.1	|- Rel A
eqreliiv.2	|- Rel B
eqreliiv.3	|- ( <. x , y >. e. A <-> <. x , y >. e. B )

Assertion

Ref	Expression
eqrelriiv	|- A = B

Distinct variable groups:   x, y, A   x, B, y

Proof of Theorem eqrelriiv

Step	Hyp	Ref	Expression
1		eqreliiv.1	. 2 |- Rel A
2		eqreliiv.2	. 2 |- Rel B
3		eqreliiv.3	. . 3 |- ( <. x , y >. e. A <-> <. x , y >. e. B )
4	3	eqrelriv 5084	. 2 |- ( ( Rel A /\ Rel B ) -> A = B )
5	1, 2, 4	mp2an 670	1 |- A = B

Syntax hints:   <-> wb 184   = wceq 1398   e. wcel 1823   <.cop 4022   Rel wrel 4993

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-9 1827  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432  ax-sep 4560  ax-nul 4568  ax-pr 4676

This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 973  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2651  df-v 3108  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3784  df-if 3930  df-sn 4017  df-pr 4019  df-op 4023  df-opab 4498  df-xp 4994  df-rel 4995

This theorem is referenced by:  eqbrriv  5086  inopab  5122  difopab  5123  dfres2  5314  restidsing  5318  cnvopab  5392  cnv0  5394  cnvdif  5397  difxp  5416  cnvcnvsn  5468  dfco2  5489  coiun  5500  co02  5504  coass  5509  ressn  5526  ovoliunlem1  22079  h2hlm  26095  cnvco1  29430  cnvco2  29431  coiun1  38172  cnviun  38173