Theorem brtxpsd2

Description: Another common abbreviation for quantifier-free definitions. (Contributed by Scott Fenton, 21-Apr-2014)

	Ref	Expression
Hypotheses	brtxpsd2.1	⊢ 𝐴 ∈ V
	brtxpsd2.2	⊢ 𝐵 ∈ V
	brtxpsd2.3	⊢ 𝑅 = ( 𝐶 ∖ ran ( ( V ⊗ E ) △ ( 𝑆 ⊗ V ) ) )
	brtxpsd2.4	⊢ 𝐴 𝐶 𝐵
Assertion	brtxpsd2	⊢ ( 𝐴 𝑅 𝐵 ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐵 ↔ 𝑥 𝑆 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		brtxpsd2.1	⊢ 𝐴 ∈ V
2		brtxpsd2.2	⊢ 𝐵 ∈ V
3		brtxpsd2.3	⊢ 𝑅 = ( 𝐶 ∖ ran ( ( V ⊗ E ) △ ( 𝑆 ⊗ V ) ) )
4		brtxpsd2.4	⊢ 𝐴 𝐶 𝐵
5	3	breqi	⊢ ( 𝐴 𝑅 𝐵 ↔ 𝐴 ( 𝐶 ∖ ran ( ( V ⊗ E ) △ ( 𝑆 ⊗ V ) ) ) 𝐵 )
6		brdif	⊢ ( 𝐴 ( 𝐶 ∖ ran ( ( V ⊗ E ) △ ( 𝑆 ⊗ V ) ) ) 𝐵 ↔ ( 𝐴 𝐶 𝐵 ∧ ¬ 𝐴 ran ( ( V ⊗ E ) △ ( 𝑆 ⊗ V ) ) 𝐵 ) )
7	5 6	bitri	⊢ ( 𝐴 𝑅 𝐵 ↔ ( 𝐴 𝐶 𝐵 ∧ ¬ 𝐴 ran ( ( V ⊗ E ) △ ( 𝑆 ⊗ V ) ) 𝐵 ) )
8	4 7	mpbiran	⊢ ( 𝐴 𝑅 𝐵 ↔ ¬ 𝐴 ran ( ( V ⊗ E ) △ ( 𝑆 ⊗ V ) ) 𝐵 )
9	1 2	brtxpsd	⊢ ( ¬ 𝐴 ran ( ( V ⊗ E ) △ ( 𝑆 ⊗ V ) ) 𝐵 ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐵 ↔ 𝑥 𝑆 𝐴 ) )
10	8 9	bitri	⊢ ( 𝐴 𝑅 𝐵 ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐵 ↔ 𝑥 𝑆 𝐴 ) )