Metamath Proof Explorer

Theorem qliftel

Description: Elementhood in the relation F . (Contributed by Mario Carneiro, 23-Dec-2016) (Revised by AV, 3-Aug-2024)

Ref Expression
Hypotheses qlift.1 ⊢ F = ran ⁡ x ∈ X ⟼ x R A
qlift.2 ⊢ φ ∧ x ∈ X → A ∈ Y
qlift.3 ⊢ φ → R Er X
qlift.4 ⊢ φ → X ∈ V
Assertion qliftel ⊢ φ → C R F D ↔ ∃ x ∈ X C R x ∧ D = A

Proof

Step Hyp Ref Expression
1 qlift.1 ⊢ F = ran ⁡ x ∈ X ⟼ x R A
2 qlift.2 ⊢ φ ∧ x ∈ X → A ∈ Y
3 qlift.3 ⊢ φ → R Er X
4 qlift.4 ⊢ φ → X ∈ V
5 1 2 3 4 qliftlem ⊢ φ ∧ x ∈ X → x R ∈ X / R
6 1 5 2 fliftel ⊢ φ → C R F D ↔ ∃ x ∈ X C R = x R ∧ D = A
7 3 adantr ⊢ φ ∧ x ∈ X → R Er X
8 simpr ⊢ φ ∧ x ∈ X → x ∈ X
9 7 8 erth2 ⊢ φ ∧ x ∈ X → C R x ↔ C R = x R
10 9 anbi1d ⊢ φ ∧ x ∈ X → C R x ∧ D = A ↔ C R = x R ∧ D = A
11 10 rexbidva ⊢ φ → ∃ x ∈ X C R x ∧ D = A ↔ ∃ x ∈ X C R = x R ∧ D = A
12 6 11 bitr4d ⊢ φ → C R F D ↔ ∃ x ∈ X C R x ∧ D = A