Step |
Hyp |
Ref |
Expression |
1 |
|
oprabex.1 |
⊢ 𝐴 ∈ V |
2 |
|
oprabex.2 |
⊢ 𝐵 ∈ V |
3 |
|
oprabex.3 |
⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) → ∃* 𝑧 𝜑 ) |
4 |
|
oprabex.4 |
⊢ 𝐹 = { 〈 〈 𝑥 , 𝑦 〉 , 𝑧 〉 ∣ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝜑 ) } |
5 |
|
moanimv |
⊢ ( ∃* 𝑧 ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝜑 ) ↔ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) → ∃* 𝑧 𝜑 ) ) |
6 |
3 5
|
mpbir |
⊢ ∃* 𝑧 ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝜑 ) |
7 |
6
|
funoprab |
⊢ Fun { 〈 〈 𝑥 , 𝑦 〉 , 𝑧 〉 ∣ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝜑 ) } |
8 |
1 2
|
xpex |
⊢ ( 𝐴 × 𝐵 ) ∈ V |
9 |
|
dmoprabss |
⊢ dom { 〈 〈 𝑥 , 𝑦 〉 , 𝑧 〉 ∣ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝜑 ) } ⊆ ( 𝐴 × 𝐵 ) |
10 |
8 9
|
ssexi |
⊢ dom { 〈 〈 𝑥 , 𝑦 〉 , 𝑧 〉 ∣ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝜑 ) } ∈ V |
11 |
|
funex |
⊢ ( ( Fun { 〈 〈 𝑥 , 𝑦 〉 , 𝑧 〉 ∣ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝜑 ) } ∧ dom { 〈 〈 𝑥 , 𝑦 〉 , 𝑧 〉 ∣ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝜑 ) } ∈ V ) → { 〈 〈 𝑥 , 𝑦 〉 , 𝑧 〉 ∣ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝜑 ) } ∈ V ) |
12 |
7 10 11
|
mp2an |
⊢ { 〈 〈 𝑥 , 𝑦 〉 , 𝑧 〉 ∣ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝜑 ) } ∈ V |
13 |
4 12
|
eqeltri |
⊢ 𝐹 ∈ V |