Metamath Proof Explorer

Theorem bj-ceqsalt0

Description: The FOL content of ceqsalt . Lemma for bj-ceqsalt and bj-ceqsaltv . (Contributed by BJ, 26-Sep-2019) (Proof modification is discouraged.)

Ref Expression
Assertion bj-ceqsalt0 ⊢ Ⅎ x ψ ∧ ∀ x θ → φ ↔ ψ ∧ ∃ x θ → ∀ x θ → φ ↔ ψ

Proof

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