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

Metamath Proof Explorer

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 ⊢ ( 𝜑 → ( 𝐶 𝐹 𝐷 ↔ ∃ 𝑥 ∈ 𝑋 ( 𝐶 = 𝐴 ∧ 𝐷 = 𝐵 ) ) )