Theorem brtxpsd

Description: Expansion of a common form used in quantifier-free definitions. (Contributed by Scott Fenton, 17-Apr-2014) (Revised by Mario Carneiro, 19-Apr-2014)

	Ref	Expression
Hypotheses	brtxpsd.1	⊢ 𝐴 ∈ V
	brtxpsd.2	⊢ 𝐵 ∈ V
Assertion	brtxpsd	⊢ ( ¬ 𝐴 ran ( ( V ⊗ E ) △ ( 𝑅 ⊗ V ) ) 𝐵 ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐵 ↔ 𝑥 𝑅 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		brtxpsd.1	⊢ 𝐴 ∈ V
2		brtxpsd.2	⊢ 𝐵 ∈ V
3		df-br	⊢ ( 𝐴 ran ( ( V ⊗ E ) △ ( 𝑅 ⊗ V ) ) 𝐵 ↔ ⟨ 𝐴 , 𝐵 ⟩ ∈ ran ( ( V ⊗ E ) △ ( 𝑅 ⊗ V ) ) )
4		opex	⊢ ⟨ 𝐴 , 𝐵 ⟩ ∈ V
5	4	elrn	⊢ ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ran ( ( V ⊗ E ) △ ( 𝑅 ⊗ V ) ) ↔ ∃ 𝑥 𝑥 ( ( V ⊗ E ) △ ( 𝑅 ⊗ V ) ) ⟨ 𝐴 , 𝐵 ⟩ )
6		brsymdif	⊢ ( 𝑥 ( ( V ⊗ E ) △ ( 𝑅 ⊗ V ) ) ⟨ 𝐴 , 𝐵 ⟩ ↔ ¬ ( 𝑥 ( V ⊗ E ) ⟨ 𝐴 , 𝐵 ⟩ ↔ 𝑥 ( 𝑅 ⊗ V ) ⟨ 𝐴 , 𝐵 ⟩ ) )
7		brv	⊢ 𝑥 V 𝐴
8		vex	⊢ 𝑥 ∈ V
9	8 1 2	brtxp	⊢ ( 𝑥 ( V ⊗ E ) ⟨ 𝐴 , 𝐵 ⟩ ↔ ( 𝑥 V 𝐴 ∧ 𝑥 E 𝐵 ) )
10	7 9	mpbiran	⊢ ( 𝑥 ( V ⊗ E ) ⟨ 𝐴 , 𝐵 ⟩ ↔ 𝑥 E 𝐵 )
11	2	epeli	⊢ ( 𝑥 E 𝐵 ↔ 𝑥 ∈ 𝐵 )
12	10 11	bitri	⊢ ( 𝑥 ( V ⊗ E ) ⟨ 𝐴 , 𝐵 ⟩ ↔ 𝑥 ∈ 𝐵 )
13		brv	⊢ 𝑥 V 𝐵
14	8 1 2	brtxp	⊢ ( 𝑥 ( 𝑅 ⊗ V ) ⟨ 𝐴 , 𝐵 ⟩ ↔ ( 𝑥 𝑅 𝐴 ∧ 𝑥 V 𝐵 ) )
15	13 14	mpbiran2	⊢ ( 𝑥 ( 𝑅 ⊗ V ) ⟨ 𝐴 , 𝐵 ⟩ ↔ 𝑥 𝑅 𝐴 )
16	12 15	bibi12i	⊢ ( ( 𝑥 ( V ⊗ E ) ⟨ 𝐴 , 𝐵 ⟩ ↔ 𝑥 ( 𝑅 ⊗ V ) ⟨ 𝐴 , 𝐵 ⟩ ) ↔ ( 𝑥 ∈ 𝐵 ↔ 𝑥 𝑅 𝐴 ) )
17	6 16	xchbinx	⊢ ( 𝑥 ( ( V ⊗ E ) △ ( 𝑅 ⊗ V ) ) ⟨ 𝐴 , 𝐵 ⟩ ↔ ¬ ( 𝑥 ∈ 𝐵 ↔ 𝑥 𝑅 𝐴 ) )
18	17	exbii	⊢ ( ∃ 𝑥 𝑥 ( ( V ⊗ E ) △ ( 𝑅 ⊗ V ) ) ⟨ 𝐴 , 𝐵 ⟩ ↔ ∃ 𝑥 ¬ ( 𝑥 ∈ 𝐵 ↔ 𝑥 𝑅 𝐴 ) )
19	5 18	bitri	⊢ ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ran ( ( V ⊗ E ) △ ( 𝑅 ⊗ V ) ) ↔ ∃ 𝑥 ¬ ( 𝑥 ∈ 𝐵 ↔ 𝑥 𝑅 𝐴 ) )
20		exnal	⊢ ( ∃ 𝑥 ¬ ( 𝑥 ∈ 𝐵 ↔ 𝑥 𝑅 𝐴 ) ↔ ¬ ∀ 𝑥 ( 𝑥 ∈ 𝐵 ↔ 𝑥 𝑅 𝐴 ) )
21	3 19 20	3bitrri	⊢ ( ¬ ∀ 𝑥 ( 𝑥 ∈ 𝐵 ↔ 𝑥 𝑅 𝐴 ) ↔ 𝐴 ran ( ( V ⊗ E ) △ ( 𝑅 ⊗ V ) ) 𝐵 )
22	21	con1bii	⊢ ( ¬ 𝐴 ran ( ( V ⊗ E ) △ ( 𝑅 ⊗ V ) ) 𝐵 ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐵 ↔ 𝑥 𝑅 𝐴 ) )