Theorem axfelem12 14957
 Description: Lemma for axfe (future) . The surreal mentioned in the previous lemma will ultimately be the union of . Again, we just change bound variables for later.
Hypothesis
Ref Expression
axfelem12.1
Assertion
Ref Expression
axfelem12
Distinct variable groups:   ,,,,,   ,,,,   ,   ,,   ,,,,   ,,,,,,   ,,   ,,,,   ,,

Proof of Theorem axfelem12
StepHypRef Expression
1 axfelem12.1 . 2
2 eqeq2 2179 . . . . . . 7
3 eqeq2 2179 . . . . . . 7
42, 3anbi12d 821 . . . . . 6
54rexbidv 2404 . . . . 5
652rexbidv 2421 . . . 4
7 reseq1 4370 . . . . . . . . 9
87eqeq1d 2178 . . . . . . . 8
98anbi1d 815 . . . . . . 7
1092rexbidv 2421 . . . . . 6
1110cbvrexv 2558 . . . . 5
12 reseq1 4370 . . . . . . . . . . 11
1312eqeq1d 2178 . . . . . . . . . 10
1413anbi2d 814 . . . . . . . . 9
1514rexbidv 2404 . . . . . . . 8
1615cbvrexv 2558 . . . . . . 7
17 reseq2 4371 . . . . . . . . . . 11
1817eqeq1d 2178 . . . . . . . . . 10
19 reseq2 4371 . . . . . . . . . . 11
2019eqeq1d 2178 . . . . . . . . . 10
2118, 20anbi12d 821 . . . . . . . . 9
2221cbvrexv 2558 . . . . . . . 8
2322rexbii 2408 . . . . . . 7
2416, 23bitri 306 . . . . . 6
2524rexbii 2408 . . . . 5
2611, 25bitri 306 . . . 4
276, 26syl6bb 324 . . 3
2827cbvabv 2692 . 2
291, 28eqtri 2190 1
 Colors of variables: wff set class Syntax hints:   wa 433   wceq 1615  cab 2157  wrex 2386   cres 4153 This theorem is referenced by:  axfelem18 14963  axfelem19 14964  axfelem20 14965  axfelem22 14967 This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1621  ax-gen 1622  ax-8 1623  ax-9 1624  ax-10 1625  ax-11 1626  ax-12 1627  ax-17 1634  ax-4 1637  ax-5o 1639  ax-6o 1642  ax-9o 1792  ax-10o 1810  ax-16 1883  ax-11o 1893  ax-ext 2152 This theorem depends on definitions:  df-bi 232  df-or 434  df-an 435  df-ex 1645  df-sb 1845  df-clab 2158  df-cleq 2163  df-clel 2166  df-rex 2390  df-v 2571  df-in 2866  df-opab 3598  df-xp 4165  df-res 4171