Metamath Proof Explorer


Theorem expandral

Description: Expand a restricted universal quantifier to primitives. (Contributed by Rohan Ridenour, 13-Aug-2023)

Ref Expression
Hypothesis expandral.1 ( 𝜑𝜓 )
Assertion expandral ( ∀ 𝑥𝐴 𝜑 ↔ ∀ 𝑥 ( 𝑥𝐴𝜓 ) )

Proof

Step Hyp Ref Expression
1 expandral.1 ( 𝜑𝜓 )
2 1 ralbii ( ∀ 𝑥𝐴 𝜑 ↔ ∀ 𝑥𝐴 𝜓 )
3 df-ral ( ∀ 𝑥𝐴 𝜓 ↔ ∀ 𝑥 ( 𝑥𝐴𝜓 ) )
4 2 3 bitri ( ∀ 𝑥𝐴 𝜑 ↔ ∀ 𝑥 ( 𝑥𝐴𝜓 ) )