Description: Existence of a set of functions. (Contributed by Paul Chapman, 25-Feb-2008) (Proof shortened by AV, 9-Jun-2025)
Ref | Expression | ||
---|---|---|---|
Hypothesis | fabexg.1 | ⊢ 𝐹 = { 𝑥 ∣ ( 𝑥 : 𝐴 ⟶ 𝐵 ∧ 𝜑 ) } | |
Assertion | fabexg | ⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ) → 𝐹 ∈ V ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | fabexg.1 | ⊢ 𝐹 = { 𝑥 ∣ ( 𝑥 : 𝐴 ⟶ 𝐵 ∧ 𝜑 ) } | |
2 | elex | ⊢ ( 𝐴 ∈ 𝐶 → 𝐴 ∈ V ) | |
3 | elex | ⊢ ( 𝐵 ∈ 𝐷 → 𝐵 ∈ V ) | |
4 | simprl | ⊢ ( ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) ∧ ( 𝑥 : 𝐴 ⟶ 𝐵 ∧ 𝜑 ) ) → 𝑥 : 𝐴 ⟶ 𝐵 ) | |
5 | simpl | ⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → 𝐴 ∈ V ) | |
6 | simpr | ⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → 𝐵 ∈ V ) | |
7 | 4 5 6 | fabexd | ⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → { 𝑥 ∣ ( 𝑥 : 𝐴 ⟶ 𝐵 ∧ 𝜑 ) } ∈ V ) |
8 | 1 7 | eqeltrid | ⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → 𝐹 ∈ V ) |
9 | 2 3 8 | syl2an | ⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ) → 𝐹 ∈ V ) |