Theorem isorel 6222

Description: An isomorphism connects binary relations via its function values. (Contributed by NM, 27-Apr-2004.)

Assertion

Ref	Expression
isorel

Proof of Theorem isorel

Dummy variables are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		df-isom 5602	. . 3
2	1	simprbi 464	. 2
3		breq1 4455	. . . 4
4		fveq2 5871	. . . . 5
5	4	breq1d 4462	. . . 4
6	3, 5	bibi12d 321	. . 3
7		breq2 4456	. . . 4
8		fveq2 5871	. . . . 5
9	8	breq2d 4464	. . . 4
10	7, 9	bibi12d 321	. . 3
11	6, 10	rspc2v 3219	. 2
12	2, 11	mpan9 469	1

Syntax hints:  ->wi 4  <->wb 184  /\wa 369  =wceq 1395  e.wcel 1818  A.wral 2807   class class class wbr 4452  -1-1-onto->wf1o 5592  `cfv 5593  Isomwiso 5594

This theorem is referenced by:  soisores  6223  isomin  6233  isoini  6234  isopolem  6241  isosolem  6243  weniso  6250  smoiso  7052  supisolem  7952  ordiso2  7961  cantnflt  8112  cantnfp1lem3  8120  cantnflem1b  8126  cantnflem1  8129  cantnfltOLD  8142  cantnfp1lem3OLD  8146  cantnflem1bOLD  8149  cantnflem1OLD  8152  wemapwe  8160  wemapweOLD  8161  cnfcomlem  8164  cnfcom  8165  cnfcom3lem  8168  cnfcomlemOLD  8172  cnfcomOLD  8173  cnfcom3lemOLD  8176  fpwwe2lem6  9034  fpwwe2lem7  9035  fpwwe2lem9  9037  leisorel  12509  seqcoll  12512  seqcoll2  12513  isercoll  13490  ordthmeolem  20302  iccpnfhmeo  21445  xrhmeo  21446  dvcnvrelem1  22418  dvcvx  22421  isoun  27520  erdszelem8  28642  erdsze2lem2  28648  fourierdlem20  31909  fourierdlem46  31935  fourierdlem50  31939  fourierdlem63  31952  fourierdlem64  31953  fourierdlem65  31954  fourierdlem76  31965  fourierdlem79  31968  fourierdlem102  31991  fourierdlem103  31992  fourierdlem104  31993  fourierdlem114  32003

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ral 2812  df-rex 2813  df-rab 2816  df-v 3111  df-dif 3478  df-un 3480  df-in 3482  df-ss 3489  df-nul 3785  df-if 3942  df-sn 4030  df-pr 4032  df-op 4036  df-uni 4250  df-br 4453  df-iota 5556  df-fv 5601  df-isom 5602