Metamath Proof Explorer


Theorem 19.32v

Description: Version of 19.32 with a disjoint variable condition, requiring fewer axioms. (Contributed by BJ, 7-Mar-2020)

Ref Expression
Assertion 19.32v ( ∀ 𝑥 ( 𝜑𝜓 ) ↔ ( 𝜑 ∨ ∀ 𝑥 𝜓 ) )

Proof

Step Hyp Ref Expression
1 19.21v ( ∀ 𝑥 ( ¬ 𝜑𝜓 ) ↔ ( ¬ 𝜑 → ∀ 𝑥 𝜓 ) )
2 df-or ( ( 𝜑𝜓 ) ↔ ( ¬ 𝜑𝜓 ) )
3 2 albii ( ∀ 𝑥 ( 𝜑𝜓 ) ↔ ∀ 𝑥 ( ¬ 𝜑𝜓 ) )
4 df-or ( ( 𝜑 ∨ ∀ 𝑥 𝜓 ) ↔ ( ¬ 𝜑 → ∀ 𝑥 𝜓 ) )
5 1 3 4 3bitr4i ( ∀ 𝑥 ( 𝜑𝜓 ) ↔ ( 𝜑 ∨ ∀ 𝑥 𝜓 ) )