Metamath Proof Explorer


Theorem brabg2

Description: Relation by a binary relation abstraction. (Contributed by Jeff Madsen, 2-Sep-2009)

Ref Expression
Hypotheses brabg2.1 ( 𝑥 = 𝐴 → ( 𝜑𝜓 ) )
brabg2.2 ( 𝑦 = 𝐵 → ( 𝜓𝜒 ) )
brabg2.3 𝑅 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 }
brabg2.4 ( 𝜒𝐴𝐶 )
Assertion brabg2 ( 𝐵𝐷 → ( 𝐴 𝑅 𝐵𝜒 ) )

Proof

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 ( 𝐵𝐷 → ( 𝐴 𝑅 𝐵𝜒 ) )