Theorem fliftel

Description: Elementhood in the relation F . (Contributed by Mario Carneiro, 23-Dec-2016)

	Ref	Expression
Hypotheses	flift.1	⊢ 𝐹 = ran ( 𝑥 ∈ 𝑋 ↦ ⟨ 𝐴 , 𝐵 ⟩ )
	flift.2	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐴 ∈ 𝑅 )
	flift.3	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐵 ∈ 𝑆 )
Assertion	fliftel	⊢ ( 𝜑 → ( 𝐶 𝐹 𝐷 ↔ ∃ 𝑥 ∈ 𝑋 ( 𝐶 = 𝐴 ∧ 𝐷 = 𝐵 ) ) )

Proof

Step	Hyp	Ref	Expression
1		flift.1	⊢ 𝐹 = ran ( 𝑥 ∈ 𝑋 ↦ ⟨ 𝐴 , 𝐵 ⟩ )
2		flift.2	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐴 ∈ 𝑅 )
3		flift.3	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐵 ∈ 𝑆 )
4		df-br	⊢ ( 𝐶 𝐹 𝐷 ↔ ⟨ 𝐶 , 𝐷 ⟩ ∈ 𝐹 )
5	1	eleq2i	⊢ ( ⟨ 𝐶 , 𝐷 ⟩ ∈ 𝐹 ↔ ⟨ 𝐶 , 𝐷 ⟩ ∈ ran ( 𝑥 ∈ 𝑋 ↦ ⟨ 𝐴 , 𝐵 ⟩ ) )
6		eqid	⊢ ( 𝑥 ∈ 𝑋 ↦ ⟨ 𝐴 , 𝐵 ⟩ ) = ( 𝑥 ∈ 𝑋 ↦ ⟨ 𝐴 , 𝐵 ⟩ )
7		opex	⊢ ⟨ 𝐴 , 𝐵 ⟩ ∈ V
8	6 7	elrnmpti	⊢ ( ⟨ 𝐶 , 𝐷 ⟩ ∈ ran ( 𝑥 ∈ 𝑋 ↦ ⟨ 𝐴 , 𝐵 ⟩ ) ↔ ∃ 𝑥 ∈ 𝑋 ⟨ 𝐶 , 𝐷 ⟩ = ⟨ 𝐴 , 𝐵 ⟩ )
9	4 5 8	3bitri	⊢ ( 𝐶 𝐹 𝐷 ↔ ∃ 𝑥 ∈ 𝑋 ⟨ 𝐶 , 𝐷 ⟩ = ⟨ 𝐴 , 𝐵 ⟩ )
10		opthg2	⊢ ( ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ) → ( ⟨ 𝐶 , 𝐷 ⟩ = ⟨ 𝐴 , 𝐵 ⟩ ↔ ( 𝐶 = 𝐴 ∧ 𝐷 = 𝐵 ) ) )
11	2 3 10	syl2anc	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( ⟨ 𝐶 , 𝐷 ⟩ = ⟨ 𝐴 , 𝐵 ⟩ ↔ ( 𝐶 = 𝐴 ∧ 𝐷 = 𝐵 ) ) )
12	11	rexbidva	⊢ ( 𝜑 → ( ∃ 𝑥 ∈ 𝑋 ⟨ 𝐶 , 𝐷 ⟩ = ⟨ 𝐴 , 𝐵 ⟩ ↔ ∃ 𝑥 ∈ 𝑋 ( 𝐶 = 𝐴 ∧ 𝐷 = 𝐵 ) ) )
13	9 12	bitrid	⊢ ( 𝜑 → ( 𝐶 𝐹 𝐷 ↔ ∃ 𝑥 ∈ 𝑋 ( 𝐶 = 𝐴 ∧ 𝐷 = 𝐵 ) ) )