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) Shorten proof and avoid ax-10 , ax-12 . (Revised by SN, 19-Dec-2024)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | funimaexg | ⊢ ( ( Fun 𝐴 ∧ 𝐵 ∈ 𝐶 ) → ( 𝐴 “ 𝐵 ) ∈ V ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | dffun6 | ⊢ ( Fun 𝐴 ↔ ( Rel 𝐴 ∧ ∀ 𝑥 ∃* 𝑦 𝑥 𝐴 𝑦 ) ) | |
| 2 | 1 | simprbi | ⊢ ( Fun 𝐴 → ∀ 𝑥 ∃* 𝑦 𝑥 𝐴 𝑦 ) |
| 3 | dfima2 | ⊢ ( 𝐴 “ 𝐵 ) = { 𝑦 ∣ ∃ 𝑥 ∈ 𝐵 𝑥 𝐴 𝑦 } | |
| 4 | axrep6g | ⊢ ( ( 𝐵 ∈ 𝐶 ∧ ∀ 𝑥 ∃* 𝑦 𝑥 𝐴 𝑦 ) → { 𝑦 ∣ ∃ 𝑥 ∈ 𝐵 𝑥 𝐴 𝑦 } ∈ V ) | |
| 5 | 3 4 | eqeltrid | ⊢ ( ( 𝐵 ∈ 𝐶 ∧ ∀ 𝑥 ∃* 𝑦 𝑥 𝐴 𝑦 ) → ( 𝐴 “ 𝐵 ) ∈ V ) |
| 6 | 2 5 | sylan2 | ⊢ ( ( 𝐵 ∈ 𝐶 ∧ Fun 𝐴 ) → ( 𝐴 “ 𝐵 ) ∈ V ) |
| 7 | 6 | ancoms | ⊢ ( ( Fun 𝐴 ∧ 𝐵 ∈ 𝐶 ) → ( 𝐴 “ 𝐵 ) ∈ V ) |