This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ( 𝐴 𝑅 𝐵 ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐵 ↔ 𝑥 𝑆 𝐴 ) )