Theorem eqrel 3245

Description: Extensionality principle for relations. Theorem 3.2(ii) of [Monk1] p. 33.

Assertion

Ref	Expression
eqrel	|- ((Rel A /\ Rel B) -> (A = B <-> A.xA.y(<.x, y>. e. A <-> <.x, y>. e. B)))

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

Proof of Theorem eqrel

Step	Hyp	Ref	Expression
1		ssrel 3242	. . 3 |- (Rel A -> (A (_ B <-> A.xA.y(<.x, y>. e. A -> <.x, y>. e. B)))
2		ssrel 3242	. . 3 |- (Rel B -> (B (_ A <-> A.xA.y(<.x, y>. e. B -> <.x, y>. e. A)))
3	1, 2	bi2anan9 631	. 2 |- ((Rel A /\ Rel B) -> ((A (_ B /\ B (_ A) <-> (A.xA.y(<.x, y>. e. A -> <.x, y>. e. B) /\ A.xA.y(<.x, y>. e. B -> <.x, y>. e. A))))
4		eqss 2073	. 2 |- (A = B <-> (A (_ B /\ B (_ A))
5		2albi 1106	. 2 |- (A.xA.y(<.x, y>. e. A <-> <.x, y>. e. B) <-> (A.xA.y(<.x, y>. e. A -> <.x, y>. e. B) /\ A.xA.y(<.x, y>. e. B -> <.x, y>. e. A)))
6	3, 4, 5	3bitr4g 554	1 |- ((Rel A /\ Rel B) -> (A = B <-> A.xA.y(<.x, y>. e. A <-> <.x, y>. e. B)))

Syntax hints:   -> wi 3   <-> wb 146   /\ wa 223  A.wal 952   = wceq 954   e. wcel 956   (_ wss 2043  <.cop 2407  Rel wrel 3170

This theorem is referenced by:  eqrelriv 3246  opabid2 3262  reldm0 3326  iss 3389  asymref 3431  intirr 3433  dfrel2 3477  cores 3491  coi1 3502  funssres 3544  fn0 3597  fcoi1 3636  fcoi2 3637  fcnvres 3639  fnopabfv 3749  eqfnfv 3788  fsn 3825

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 960  ax-gen 961  ax-8 962  ax-10 964  ax-11 965  ax-12 966  ax-13 967  ax-14 968  ax-17 969  ax-4 971  ax-5o 973  ax-6o 976  ax-9o 1121  ax-10o 1138  ax-16 1208  ax-11o 1216  ax-ext 1457  ax-sep 2698  ax-pow 2737  ax-pr 2774

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 979  df-sb 1170  df-eu 1380  df-mo 1381  df-clab 1462  df-cleq 1467  df-clel 1470  df-ne 1584  df-v 1808  df-dif 2045  df-un 2046  df-in 2047  df-ss 2049  df-nul 2277  df-pw 2398  df-sn 2408  df-pr 2409  df-op 2412  df-opab 2662  df-xp 3179  df-rel 3180

Copyright terms: Public domain