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