Theorem eqrelriiv 5214

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

Syntax hints:   <-> wb 196   = wceq 1483   e. wcel 1990   <.cop 4183   Rel wrel 5119

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-in 3581  df-ss 3588  df-opab 4713  df-xp 5120  df-rel 5121

This theorem is referenced by:  eqbrriv  5215  inopab  5252  difopab  5253  dfres2  5453  restidsing  5458  restidsingOLD  5459  cnvopab  5533  cnv0OLD  5536  cnvdif  5539  difxp  5558  cnvcnvsn  5612  dfco2  5634  coiun  5645  co02  5649  coass  5654  ressn  5671  ovoliunlem1  23270  h2hlm  27837  cnvco1  31649  cnvco2  31650  inxprnres  34060  cnviun  37942  coiun1  37944