Theorem r2al 3174

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 1939	. 2 ⊢ (∀𝑦(𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐵 → 𝜑)) ↔ (𝑥 ∈ 𝐴 → ∀𝑦(𝑦 ∈ 𝐵 → 𝜑)))
2	1	r2allem 3122	1 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 ↔ ∀𝑥∀𝑦((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝜑))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395  ∀wal 1538   ∈ wcel 2109  ∀wral 3045

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-ral 3046

This theorem is referenced by:  r2ex  3175  r3al  3176  ralcom  3266  nfra2w  3276  moel  3378  raliunxp  5806  codir  6096  qfto  6097  dfpo2  6272  fununi  6594  dff13  7232  mpo2eqb  7524  frpoins3xpg  8122  xpord2indlem  8129  tz7.48lem  8412  qliftfun  8778  zorn2lem4  10459  isirred2  20337  isdomn3  20631  cnmpt12  23561  cnmpt22  23568  dchrelbas3  27156  cvmlift2lem12  35308  dfso2  35749  r2alan  38245  inxpss  38306  inxpss3  38309  dfac5prim  44987  permac8prim  45011  iscnrm3lem2  48927  joindm2  48960  meetdm2  48962