Theorem r2al 3169

Description: Double restricted universal quantification. (Contributed by NM, 19-Nov-1995.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 9-Jan-2020.)

Assertion

Ref	Expression
r2al	⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 ↔ ∀𝑥∀𝑦((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝜑))

Distinct variable groups:   𝑥,𝑦   𝑦,𝐴

Allowed substitution hints:   𝜑(𝑥,𝑦)   𝐴(𝑥)   𝐵(𝑥,𝑦)

Proof of Theorem r2al

Step	Hyp	Ref	Expression
1		19.21v 1940	. 2 ⊢ (∀𝑦(𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐵 → 𝜑)) ↔ (𝑥 ∈ 𝐴 → ∀𝑦(𝑦 ∈ 𝐵 → 𝜑)))
2	1	r2allem 3121	1 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 ↔ ∀𝑥∀𝑦((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝜑))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395  ∀wal 1539   ∈ wcel 2113  ∀wral 3048

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-ral 3049

This theorem is referenced by:  r2ex  3170  r3al  3171  ralcom  3261  nfra2w  3269  moel  3367  raliunxp  5783  codir  6071  qfto  6072  dfpo2  6248  fununi  6561  dff13  7194  mpo2eqb  7484  frpoins3xpg  8076  xpord2indlem  8083  tz7.48lem  8366  qliftfun  8732  zorn2lem4  10397  isirred2  20341  isdomn3  20632  cnmpt12  23583  cnmpt22  23590  dchrelbas3  27177  cvmlift2lem12  35379  dfso2  35820  r2alan  38306  inxpss  38369  inxpss3  38372  dfac5prim  45107  permac8prim  45131  iscnrm3lem2  49059  joindm2  49092  meetdm2  49094