Step |
Hyp |
Ref |
Expression |
1 |
|
brabg2.1 |
⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) ) |
2 |
|
brabg2.2 |
⊢ ( 𝑦 = 𝐵 → ( 𝜓 ↔ 𝜒 ) ) |
3 |
|
brabg2.3 |
⊢ 𝑅 = { 〈 𝑥 , 𝑦 〉 ∣ 𝜑 } |
4 |
|
brabg2.4 |
⊢ ( 𝜒 → 𝐴 ∈ 𝐶 ) |
5 |
3
|
relopabiv |
⊢ Rel 𝑅 |
6 |
5
|
brrelex1i |
⊢ ( 𝐴 𝑅 𝐵 → 𝐴 ∈ V ) |
7 |
1 2 3
|
brabg |
⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ 𝐷 ) → ( 𝐴 𝑅 𝐵 ↔ 𝜒 ) ) |
8 |
7
|
biimpd |
⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ 𝐷 ) → ( 𝐴 𝑅 𝐵 → 𝜒 ) ) |
9 |
8
|
ex |
⊢ ( 𝐴 ∈ V → ( 𝐵 ∈ 𝐷 → ( 𝐴 𝑅 𝐵 → 𝜒 ) ) ) |
10 |
9
|
com3l |
⊢ ( 𝐵 ∈ 𝐷 → ( 𝐴 𝑅 𝐵 → ( 𝐴 ∈ V → 𝜒 ) ) ) |
11 |
6 10
|
mpdi |
⊢ ( 𝐵 ∈ 𝐷 → ( 𝐴 𝑅 𝐵 → 𝜒 ) ) |
12 |
1 2 3
|
brabg |
⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ) → ( 𝐴 𝑅 𝐵 ↔ 𝜒 ) ) |
13 |
12
|
exbiri |
⊢ ( 𝐴 ∈ 𝐶 → ( 𝐵 ∈ 𝐷 → ( 𝜒 → 𝐴 𝑅 𝐵 ) ) ) |
14 |
13
|
com3l |
⊢ ( 𝐵 ∈ 𝐷 → ( 𝜒 → ( 𝐴 ∈ 𝐶 → 𝐴 𝑅 𝐵 ) ) ) |
15 |
4 14
|
mpdi |
⊢ ( 𝐵 ∈ 𝐷 → ( 𝜒 → 𝐴 𝑅 𝐵 ) ) |
16 |
11 15
|
impbid |
⊢ ( 𝐵 ∈ 𝐷 → ( 𝐴 𝑅 𝐵 ↔ 𝜒 ) ) |