Step |
Hyp |
Ref |
Expression |
1 |
|
brfvopabrbr.1 |
⊢ ( 𝐴 ‘ 𝑍 ) = { 〈 𝑥 , 𝑦 〉 ∣ ( 𝑥 ( 𝐵 ‘ 𝑍 ) 𝑦 ∧ 𝜑 ) } |
2 |
|
brfvopabrbr.2 |
⊢ ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) → ( 𝜑 ↔ 𝜓 ) ) |
3 |
|
brfvopabrbr.3 |
⊢ Rel ( 𝐵 ‘ 𝑍 ) |
4 |
|
brne0 |
⊢ ( 𝑋 ( 𝐴 ‘ 𝑍 ) 𝑌 → ( 𝐴 ‘ 𝑍 ) ≠ ∅ ) |
5 |
|
fvprc |
⊢ ( ¬ 𝑍 ∈ V → ( 𝐴 ‘ 𝑍 ) = ∅ ) |
6 |
5
|
necon1ai |
⊢ ( ( 𝐴 ‘ 𝑍 ) ≠ ∅ → 𝑍 ∈ V ) |
7 |
4 6
|
syl |
⊢ ( 𝑋 ( 𝐴 ‘ 𝑍 ) 𝑌 → 𝑍 ∈ V ) |
8 |
1
|
relopabiv |
⊢ Rel ( 𝐴 ‘ 𝑍 ) |
9 |
8
|
brrelex1i |
⊢ ( 𝑋 ( 𝐴 ‘ 𝑍 ) 𝑌 → 𝑋 ∈ V ) |
10 |
8
|
brrelex2i |
⊢ ( 𝑋 ( 𝐴 ‘ 𝑍 ) 𝑌 → 𝑌 ∈ V ) |
11 |
7 9 10
|
3jca |
⊢ ( 𝑋 ( 𝐴 ‘ 𝑍 ) 𝑌 → ( 𝑍 ∈ V ∧ 𝑋 ∈ V ∧ 𝑌 ∈ V ) ) |
12 |
|
brne0 |
⊢ ( 𝑋 ( 𝐵 ‘ 𝑍 ) 𝑌 → ( 𝐵 ‘ 𝑍 ) ≠ ∅ ) |
13 |
|
fvprc |
⊢ ( ¬ 𝑍 ∈ V → ( 𝐵 ‘ 𝑍 ) = ∅ ) |
14 |
13
|
necon1ai |
⊢ ( ( 𝐵 ‘ 𝑍 ) ≠ ∅ → 𝑍 ∈ V ) |
15 |
12 14
|
syl |
⊢ ( 𝑋 ( 𝐵 ‘ 𝑍 ) 𝑌 → 𝑍 ∈ V ) |
16 |
3
|
brrelex1i |
⊢ ( 𝑋 ( 𝐵 ‘ 𝑍 ) 𝑌 → 𝑋 ∈ V ) |
17 |
3
|
brrelex2i |
⊢ ( 𝑋 ( 𝐵 ‘ 𝑍 ) 𝑌 → 𝑌 ∈ V ) |
18 |
15 16 17
|
3jca |
⊢ ( 𝑋 ( 𝐵 ‘ 𝑍 ) 𝑌 → ( 𝑍 ∈ V ∧ 𝑋 ∈ V ∧ 𝑌 ∈ V ) ) |
19 |
18
|
adantr |
⊢ ( ( 𝑋 ( 𝐵 ‘ 𝑍 ) 𝑌 ∧ 𝜓 ) → ( 𝑍 ∈ V ∧ 𝑋 ∈ V ∧ 𝑌 ∈ V ) ) |
20 |
1
|
a1i |
⊢ ( 𝑍 ∈ V → ( 𝐴 ‘ 𝑍 ) = { 〈 𝑥 , 𝑦 〉 ∣ ( 𝑥 ( 𝐵 ‘ 𝑍 ) 𝑦 ∧ 𝜑 ) } ) |
21 |
20 2
|
rbropap |
⊢ ( ( 𝑍 ∈ V ∧ 𝑋 ∈ V ∧ 𝑌 ∈ V ) → ( 𝑋 ( 𝐴 ‘ 𝑍 ) 𝑌 ↔ ( 𝑋 ( 𝐵 ‘ 𝑍 ) 𝑌 ∧ 𝜓 ) ) ) |
22 |
11 19 21
|
pm5.21nii |
⊢ ( 𝑋 ( 𝐴 ‘ 𝑍 ) 𝑌 ↔ ( 𝑋 ( 𝐵 ‘ 𝑍 ) 𝑌 ∧ 𝜓 ) ) |