Metamath Proof Explorer


Theorem expanduniss

Description: Expand U. A C_ B to primitives. (Contributed by Rohan Ridenour, 13-Aug-2023)

Ref Expression
Assertion expanduniss ( 𝐴𝐵 ↔ ∀ 𝑥 ( 𝑥𝐴 → ∀ 𝑦 ( 𝑦𝑥𝑦𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 unissb ( 𝐴𝐵 ↔ ∀ 𝑥𝐴 𝑥𝐵 )
2 dfss2 ( 𝑥𝐵 ↔ ∀ 𝑦 ( 𝑦𝑥𝑦𝐵 ) )
3 2 expandral ( ∀ 𝑥𝐴 𝑥𝐵 ↔ ∀ 𝑥 ( 𝑥𝐴 → ∀ 𝑦 ( 𝑦𝑥𝑦𝐵 ) ) )
4 1 3 bitri ( 𝐴𝐵 ↔ ∀ 𝑥 ( 𝑥𝐴 → ∀ 𝑦 ( 𝑦𝑥𝑦𝐵 ) ) )