Theorem eqrelriiv 4928

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 4927	. 2 |- ( ( Rel A /\ Rel B ) -> A = B )
5	1, 2, 4	mp2an 677	1 |- A = B

Syntax hints:   <-> wb 188   = wceq 1443   e. wcel 1886   <.cop 3973   Rel wrel 4838

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1668  ax-4 1681  ax-5 1757  ax-6 1804  ax-7 1850  ax-9 1895  ax-10 1914  ax-11 1919  ax-12 1932  ax-13 2090  ax-ext 2430  ax-sep 4524  ax-nul 4533  ax-pr 4638

This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3an 986  df-tru 1446  df-ex 1663  df-nf 1667  df-sb 1797  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2580  df-ne 2623  df-v 3046  df-dif 3406  df-un 3408  df-in 3410  df-ss 3417  df-nul 3731  df-if 3881  df-sn 3968  df-pr 3970  df-op 3974  df-opab 4461  df-xp 4839  df-rel 4840

This theorem is referenced by:  eqbrriv  4929  inopab  4964  difopab  4965  dfres2  5156  restidsing  5160  cnvopab  5236  cnv0  5238  cnvdif  5241  difxp  5260  cnvcnvsn  5312  dfco2  5333  coiun  5344  co02  5348  coass  5353  ressn  5371  ovoliunlem1  22448  h2hlm  26626  cnvco1  30393  cnvco2  30394  cnviun  36236  coiun1  36238