Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  funimaexg Structured version   Visualization version   GIF version

Theorem funimaexg 6421
 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 𝐴𝐵𝐶) → (𝐴𝐵) ∈ V)

Proof of Theorem funimaexg
Dummy variables 𝑤 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 imaeq2 5897 . . . . 5 (𝑤 = 𝐵 → (𝐴𝑤) = (𝐴𝐵))
21eleq1d 2836 . . . 4 (𝑤 = 𝐵 → ((𝐴𝑤) ∈ V ↔ (𝐴𝐵) ∈ V))
32imbi2d 344 . . 3 (𝑤 = 𝐵 → ((Fun 𝐴 → (𝐴𝑤) ∈ V) ↔ (Fun 𝐴 → (𝐴𝐵) ∈ V)))
4 dffun5 6348 . . . 4 (Fun 𝐴 ↔ (Rel 𝐴 ∧ ∀𝑥𝑧𝑦(⟨𝑥, 𝑦⟩ ∈ 𝐴𝑦 = 𝑧)))
5 nfv 1915 . . . . . 6 𝑧𝑥, 𝑦⟩ ∈ 𝐴
65axrep4 5161 . . . . 5 (∀𝑥𝑧𝑦(⟨𝑥, 𝑦⟩ ∈ 𝐴𝑦 = 𝑧) → ∃𝑧𝑦(𝑦𝑧 ↔ ∃𝑥(𝑥𝑤 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐴)))
7 isset 3422 . . . . . 6 ((𝐴𝑤) ∈ V ↔ ∃𝑧 𝑧 = (𝐴𝑤))
8 dfima3 5904 . . . . . . . . 9 (𝐴𝑤) = {𝑦 ∣ ∃𝑥(𝑥𝑤 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐴)}
98eqeq2i 2771 . . . . . . . 8 (𝑧 = (𝐴𝑤) ↔ 𝑧 = {𝑦 ∣ ∃𝑥(𝑥𝑤 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐴)})
10 abeq2 2884 . . . . . . . 8 (𝑧 = {𝑦 ∣ ∃𝑥(𝑥𝑤 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐴)} ↔ ∀𝑦(𝑦𝑧 ↔ ∃𝑥(𝑥𝑤 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐴)))
119, 10bitri 278 . . . . . . 7 (𝑧 = (𝐴𝑤) ↔ ∀𝑦(𝑦𝑧 ↔ ∃𝑥(𝑥𝑤 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐴)))
1211exbii 1849 . . . . . 6 (∃𝑧 𝑧 = (𝐴𝑤) ↔ ∃𝑧𝑦(𝑦𝑧 ↔ ∃𝑥(𝑥𝑤 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐴)))
137, 12bitri 278 . . . . 5 ((𝐴𝑤) ∈ V ↔ ∃𝑧𝑦(𝑦𝑧 ↔ ∃𝑥(𝑥𝑤 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐴)))
146, 13sylibr 237 . . . 4 (∀𝑥𝑧𝑦(⟨𝑥, 𝑦⟩ ∈ 𝐴𝑦 = 𝑧) → (𝐴𝑤) ∈ V)
154, 14simplbiim 508 . . 3 (Fun 𝐴 → (𝐴𝑤) ∈ V)
163, 15vtoclg 3485 . 2 (𝐵𝐶 → (Fun 𝐴 → (𝐴𝐵) ∈ V))
1716impcom 411 1 ((Fun 𝐴𝐵𝐶) → (𝐴𝐵) ∈ V)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399  ∀wal 1536   = wceq 1538  ∃wex 1781   ∈ wcel 2111  {cab 2735  Vcvv 3409  ⟨cop 4528   “ cima 5527  Rel wrel 5529  Fun wfun 6329 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2729  ax-rep 5156  ax-sep 5169  ax-nul 5176  ax-pr 5298 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2557  df-eu 2588  df-clab 2736  df-cleq 2750  df-clel 2830  df-nfc 2901  df-ral 3075  df-rex 3076  df-rab 3079  df-v 3411  df-dif 3861  df-un 3863  df-in 3865  df-ss 3875  df-nul 4226  df-if 4421  df-sn 4523  df-pr 4525  df-op 4529  df-br 5033  df-opab 5095  df-id 5430  df-xp 5530  df-cnv 5532  df-co 5533  df-dm 5534  df-rn 5535  df-res 5536  df-ima 5537  df-fun 6337 This theorem is referenced by:  funimaex  6422  resfunexg  6969  resfunexgALT  7653  fnexALT  7656  wdomimag  9084  carduniima  9556  dfac12lem2  9604  ttukeylem3  9971  nnexALT  11676  seqex  13420  fbasrn  22584  elfm3  22650  bdayimaon  33461  nosupno  33471  noinfno  33486  noeta2  33544  etasslt2  33569  scutbdaybnd2lim  33572  madeval  33596  oldval  33598  fundcmpsurinjlem3  44285  fundcmpsurbijinjpreimafv  44292  fundcmpsurbijinj  44295  fundcmpsurinjALT  44297
 Copyright terms: Public domain W3C validator