ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  funimaexg Structured version   GIF version

Theorem funimaexg 4897
Description: Axiom of Replacement using abbreviations. Axiom 39(vi) of [Quine] p. 284. Compare Exercise 9 of [TakeutiZaring] p. 29. (Contributed by NM, 10-Sep-2006.)
Assertion
Ref Expression
funimaexg ((Fun A B 𝐶) → (AB) V)

Proof of Theorem funimaexg
StepHypRef Expression
1 simpl 102 . . 3 ((Fun A B 𝐶) → Fun A)
2 funrel 4833 . . 3 (Fun A → Rel A)
3 resres 4539 . . . . . . 7 ((A ↾ dom A) ↾ B) = (A ↾ (dom AB))
4 incom 3097 . . . . . . . 8 (B ∩ dom A) = (dom AB)
54reseq2i 4524 . . . . . . 7 (A ↾ (B ∩ dom A)) = (A ↾ (dom AB))
63, 5eqtr4i 2036 . . . . . 6 ((A ↾ dom A) ↾ B) = (A ↾ (B ∩ dom A))
7 resdm 4564 . . . . . . 7 (Rel A → (A ↾ dom A) = A)
87reseq1d 4526 . . . . . 6 (Rel A → ((A ↾ dom A) ↾ B) = (AB))
96, 8syl5eqr 2059 . . . . 5 (Rel A → (A ↾ (B ∩ dom A)) = (AB))
109rneqd 4478 . . . 4 (Rel A → ran (A ↾ (B ∩ dom A)) = ran (AB))
11 df-ima 4273 . . . 4 (A “ (B ∩ dom A)) = ran (A ↾ (B ∩ dom A))
12 df-ima 4273 . . . 4 (AB) = ran (AB)
1310, 11, 123eqtr4g 2070 . . 3 (Rel A → (A “ (B ∩ dom A)) = (AB))
141, 2, 133syl 17 . 2 ((Fun A B 𝐶) → (A “ (B ∩ dom A)) = (AB))
15 inex1g 3856 . . 3 (B 𝐶 → (B ∩ dom A) V)
16 inss2 3126 . . . 4 (B ∩ dom A) ⊆ dom A
17 funimaexglem 4896 . . . 4 ((Fun A (B ∩ dom A) V (B ∩ dom A) ⊆ dom A) → (A “ (B ∩ dom A)) V)
1816, 17mp3an3 1201 . . 3 ((Fun A (B ∩ dom A) V) → (A “ (B ∩ dom A)) V)
1915, 18sylan2 270 . 2 ((Fun A B 𝐶) → (A “ (B ∩ dom A)) V)
2014, 19eqeltrrd 2088 1 ((Fun A B 𝐶) → (AB) V)
Colors of variables: wff set class
Syntax hints:  wi 4   wa 97   = wceq 1223   wcel 1366  Vcvv 2526  cin 2884  wss 2885  dom cdm 4260  ran crn 4261  cres 4262  cima 4263  Rel wrel 4265  Fun wfun 4811
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 614  ax-5 1309  ax-7 1310  ax-gen 1311  ax-ie1 1355  ax-ie2 1356  ax-8 1368  ax-10 1369  ax-11 1370  ax-i12 1371  ax-bnd 1372  ax-4 1373  ax-14 1378  ax-17 1392  ax-i9 1396  ax-ial 1400  ax-i5r 1401  ax-ext 1995  ax-coll 3835  ax-sep 3838  ax-pow 3890  ax-pr 3907
This theorem depends on definitions:  df-bi 110  df-3an 869  df-tru 1226  df-nf 1323  df-sb 1619  df-eu 1876  df-mo 1877  df-clab 2000  df-cleq 2006  df-clel 2009  df-nfc 2140  df-ral 2280  df-rex 2281  df-v 2528  df-un 2890  df-in 2892  df-ss 2899  df-pw 3325  df-sn 3345  df-pr 3346  df-op 3348  df-br 3728  df-opab 3782  df-id 3993  df-xp 4266  df-rel 4267  df-cnv 4268  df-co 4269  df-dm 4270  df-rn 4271  df-res 4272  df-ima 4273  df-fun 4819
This theorem is referenced by:  funimaex  4898  resfunexg  5295  resfunexgALT  5648  fnexALT  5651
  Copyright terms: Public domain W3C validator