Theorem eqrelriv 3311

Description: Inference from extensionality principle for relations.

Hypotheses

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

Assertion

Ref	Expression
eqrelriv	|- A = B

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

Proof of Theorem eqrelriv

Step	Hyp	Ref	Expression
1		eqreli.1	. . 3 |- Rel A
2		eqreli.2	. . 3 |- Rel B
3		eqrel 3308	. . 3 |- ((Rel A /\ Rel B) -> (A = B <-> A.xA.y(<.x, y>. e. A <-> <.x, y>. e. B)))
4	1, 2, 3	mp2an 700	. 2 |- (A = B <-> A.xA.y(<.x, y>. e. A <-> <.x, y>. e. B))
5		eqreli.3	. . 3 |- (<.x, y>. e. A <-> <.x, y>. e. B)
6	5	ax-gen 995	. 2 |- A.y(<.x, y>. e. A <-> <.x, y>. e. B)
7	4, 6	mpgbir 1020	1 |- A = B

Syntax hints:   <-> wb 144  A.wal 986   = wceq 988   e. wcel 990  <.cop 2456  Rel wrel 3230

This theorem is referenced by:  eqbrriv 3312  inopab 3334  inxp 3335  cnvopab 3508  cnv0 3509  cnvi 3510  cnvun 3511  cnvin 3512  cnvxp 3520  cnvsn 3551  dfco2 3568  coiun 3578  co02 3582  coass 3586  sbthcl 4546

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 994  ax-gen 995  ax-8 996  ax-10 998  ax-11 999  ax-12 1000  ax-13 1001  ax-14 1002  ax-17 1003  ax-4 1005  ax-5o 1007  ax-6o 1010  ax-9o 1155  ax-10o 1173  ax-16 1243  ax-11o 1251  ax-ext 1494  ax-sep 2754  ax-pow 2794  ax-pr 2832

This theorem depends on definitions:  df-bi 145  df-or 222  df-an 223  df-ex 1013  df-sb 1205  df-eu 1415  df-mo 1416  df-clab 1500  df-cleq 1505  df-clel 1508  df-ne 1624  df-v 1850  df-dif 2093  df-un 2094  df-in 2095  df-ss 2097  df-nul 2325  df-pw 2447  df-sn 2457  df-pr 2458  df-op 2461  df-opab 2718  df-xp 3239  df-rel 3240

Copyright terms: Public domain