Step |
Hyp |
Ref |
Expression |
1 |
|
fvopab3ig.1 |
⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) ) |
2 |
|
fvopab3ig.2 |
⊢ ( 𝑦 = 𝐵 → ( 𝜓 ↔ 𝜒 ) ) |
3 |
|
fvopab3ig.3 |
⊢ ( 𝑥 ∈ 𝐶 → ∃* 𝑦 𝜑 ) |
4 |
|
fvopab3ig.4 |
⊢ 𝐹 = { 〈 𝑥 , 𝑦 〉 ∣ ( 𝑥 ∈ 𝐶 ∧ 𝜑 ) } |
5 |
|
eleq1 |
⊢ ( 𝑥 = 𝐴 → ( 𝑥 ∈ 𝐶 ↔ 𝐴 ∈ 𝐶 ) ) |
6 |
5 1
|
anbi12d |
⊢ ( 𝑥 = 𝐴 → ( ( 𝑥 ∈ 𝐶 ∧ 𝜑 ) ↔ ( 𝐴 ∈ 𝐶 ∧ 𝜓 ) ) ) |
7 |
2
|
anbi2d |
⊢ ( 𝑦 = 𝐵 → ( ( 𝐴 ∈ 𝐶 ∧ 𝜓 ) ↔ ( 𝐴 ∈ 𝐶 ∧ 𝜒 ) ) ) |
8 |
6 7
|
opelopabg |
⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ) → ( 〈 𝐴 , 𝐵 〉 ∈ { 〈 𝑥 , 𝑦 〉 ∣ ( 𝑥 ∈ 𝐶 ∧ 𝜑 ) } ↔ ( 𝐴 ∈ 𝐶 ∧ 𝜒 ) ) ) |
9 |
8
|
biimpar |
⊢ ( ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ) ∧ ( 𝐴 ∈ 𝐶 ∧ 𝜒 ) ) → 〈 𝐴 , 𝐵 〉 ∈ { 〈 𝑥 , 𝑦 〉 ∣ ( 𝑥 ∈ 𝐶 ∧ 𝜑 ) } ) |
10 |
9
|
exp43 |
⊢ ( 𝐴 ∈ 𝐶 → ( 𝐵 ∈ 𝐷 → ( 𝐴 ∈ 𝐶 → ( 𝜒 → 〈 𝐴 , 𝐵 〉 ∈ { 〈 𝑥 , 𝑦 〉 ∣ ( 𝑥 ∈ 𝐶 ∧ 𝜑 ) } ) ) ) ) |
11 |
10
|
pm2.43a |
⊢ ( 𝐴 ∈ 𝐶 → ( 𝐵 ∈ 𝐷 → ( 𝜒 → 〈 𝐴 , 𝐵 〉 ∈ { 〈 𝑥 , 𝑦 〉 ∣ ( 𝑥 ∈ 𝐶 ∧ 𝜑 ) } ) ) ) |
12 |
11
|
imp |
⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ) → ( 𝜒 → 〈 𝐴 , 𝐵 〉 ∈ { 〈 𝑥 , 𝑦 〉 ∣ ( 𝑥 ∈ 𝐶 ∧ 𝜑 ) } ) ) |
13 |
4
|
fveq1i |
⊢ ( 𝐹 ‘ 𝐴 ) = ( { 〈 𝑥 , 𝑦 〉 ∣ ( 𝑥 ∈ 𝐶 ∧ 𝜑 ) } ‘ 𝐴 ) |
14 |
|
funopab |
⊢ ( Fun { 〈 𝑥 , 𝑦 〉 ∣ ( 𝑥 ∈ 𝐶 ∧ 𝜑 ) } ↔ ∀ 𝑥 ∃* 𝑦 ( 𝑥 ∈ 𝐶 ∧ 𝜑 ) ) |
15 |
|
moanimv |
⊢ ( ∃* 𝑦 ( 𝑥 ∈ 𝐶 ∧ 𝜑 ) ↔ ( 𝑥 ∈ 𝐶 → ∃* 𝑦 𝜑 ) ) |
16 |
3 15
|
mpbir |
⊢ ∃* 𝑦 ( 𝑥 ∈ 𝐶 ∧ 𝜑 ) |
17 |
14 16
|
mpgbir |
⊢ Fun { 〈 𝑥 , 𝑦 〉 ∣ ( 𝑥 ∈ 𝐶 ∧ 𝜑 ) } |
18 |
|
funopfv |
⊢ ( Fun { 〈 𝑥 , 𝑦 〉 ∣ ( 𝑥 ∈ 𝐶 ∧ 𝜑 ) } → ( 〈 𝐴 , 𝐵 〉 ∈ { 〈 𝑥 , 𝑦 〉 ∣ ( 𝑥 ∈ 𝐶 ∧ 𝜑 ) } → ( { 〈 𝑥 , 𝑦 〉 ∣ ( 𝑥 ∈ 𝐶 ∧ 𝜑 ) } ‘ 𝐴 ) = 𝐵 ) ) |
19 |
17 18
|
ax-mp |
⊢ ( 〈 𝐴 , 𝐵 〉 ∈ { 〈 𝑥 , 𝑦 〉 ∣ ( 𝑥 ∈ 𝐶 ∧ 𝜑 ) } → ( { 〈 𝑥 , 𝑦 〉 ∣ ( 𝑥 ∈ 𝐶 ∧ 𝜑 ) } ‘ 𝐴 ) = 𝐵 ) |
20 |
13 19
|
eqtrid |
⊢ ( 〈 𝐴 , 𝐵 〉 ∈ { 〈 𝑥 , 𝑦 〉 ∣ ( 𝑥 ∈ 𝐶 ∧ 𝜑 ) } → ( 𝐹 ‘ 𝐴 ) = 𝐵 ) |
21 |
12 20
|
syl6 |
⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ) → ( 𝜒 → ( 𝐹 ‘ 𝐴 ) = 𝐵 ) ) |