Metamath Proof Explorer

Theorem bj-ceqsalt1

Description: The FOL content of ceqsalt . Lemma for bj-ceqsalt and bj-ceqsaltv . TODO: consider removing if it does not add anything to bj-ceqsalt0 . (Contributed by BJ, 26-Sep-2019) (Proof modification is discouraged.)

Ref Expression
Hypothesis bj-ceqsalt1.1 ⊢ θ → ∃ x χ
Assertion bj-ceqsalt1 ⊢ Ⅎ x ψ ∧ ∀ x χ → φ ↔ ψ ∧ θ → ∀ x χ → φ ↔ ψ

Proof

Step Hyp Ref Expression
1 bj-ceqsalt1.1 ⊢ θ → ∃ x χ
2 1 3ad2ant3 ⊢ Ⅎ x ψ ∧ ∀ x χ → φ ↔ ψ ∧ θ → ∃ x χ
3 biimp ⊢ φ ↔ ψ → φ → ψ
4 3 imim3i ⊢ χ → φ ↔ ψ → χ → φ → χ → ψ
5 4 al2imi ⊢ ∀ x χ → φ ↔ ψ → ∀ x χ → φ → ∀ x χ → ψ
6 5 3ad2ant2 ⊢ Ⅎ x ψ ∧ ∀ x χ → φ ↔ ψ ∧ θ → ∀ x χ → φ → ∀ x χ → ψ
7 19.23t ⊢ Ⅎ x ψ → ∀ x χ → ψ ↔ ∃ x χ → ψ
8 7 3ad2ant1 ⊢ Ⅎ x ψ ∧ ∀ x χ → φ ↔ ψ ∧ θ → ∀ x χ → ψ ↔ ∃ x χ → ψ
9 6 8 sylibd ⊢ Ⅎ x ψ ∧ ∀ x χ → φ ↔ ψ ∧ θ → ∀ x χ → φ → ∃ x χ → ψ
10 2 9 mpid ⊢ Ⅎ x ψ ∧ ∀ x χ → φ ↔ ψ ∧ θ → ∀ x χ → φ → ψ
11 biimpr ⊢ φ ↔ ψ → ψ → φ
12 11 imim2i ⊢ χ → φ ↔ ψ → χ → ψ → φ
13 12 com23 ⊢ χ → φ ↔ ψ → ψ → χ → φ
14 13 alimi ⊢ ∀ x χ → φ ↔ ψ → ∀ x ψ → χ → φ
15 14 3ad2ant2 ⊢ Ⅎ x ψ ∧ ∀ x χ → φ ↔ ψ ∧ θ → ∀ x ψ → χ → φ
16 19.21t ⊢ Ⅎ x ψ → ∀ x ψ → χ → φ ↔ ψ → ∀ x χ → φ
17 16 3ad2ant1 ⊢ Ⅎ x ψ ∧ ∀ x χ → φ ↔ ψ ∧ θ → ∀ x ψ → χ → φ ↔ ψ → ∀ x χ → φ
18 15 17 mpbid ⊢ Ⅎ x ψ ∧ ∀ x χ → φ ↔ ψ ∧ θ → ψ → ∀ x χ → φ
19 10 18 impbid ⊢ Ⅎ x ψ ∧ ∀ x χ → φ ↔ ψ ∧ θ → ∀ x χ → φ ↔ ψ