Theorem brtxpsd3

Description: A third common abbreviation for quantifier-free definitions. (Contributed by Scott Fenton, 3-May-2014)

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

Proof

Step	Hyp	Ref	Expression
1		brtxpsd2.1	⊢ 𝐴 ∈ V
2		brtxpsd2.2	⊢ 𝐵 ∈ V
3		brtxpsd2.3	⊢ 𝑅 = ( 𝐶 ∖ ran ( ( V ⊗ E ) △ ( 𝑆 ⊗ V ) ) )
4		brtxpsd2.4	⊢ 𝐴 𝐶 𝐵
5		brtxpsd3.5	⊢ ( 𝑥 ∈ 𝑋 ↔ 𝑥 𝑆 𝐴 )
6	5	bibi2i	⊢ ( ( 𝑥 ∈ 𝐵 ↔ 𝑥 ∈ 𝑋 ) ↔ ( 𝑥 ∈ 𝐵 ↔ 𝑥 𝑆 𝐴 ) )
7	6	albii	⊢ ( ∀ 𝑥 ( 𝑥 ∈ 𝐵 ↔ 𝑥 ∈ 𝑋 ) ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐵 ↔ 𝑥 𝑆 𝐴 ) )
8		dfcleq	⊢ ( 𝐵 = 𝑋 ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐵 ↔ 𝑥 ∈ 𝑋 ) )
9	1 2 3 4	brtxpsd2	⊢ ( 𝐴 𝑅 𝐵 ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐵 ↔ 𝑥 𝑆 𝐴 ) )
10	7 8 9	3bitr4ri	⊢ ( 𝐴 𝑅 𝐵 ↔ 𝐵 = 𝑋 )