Theorem r2al 3201

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

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400  ∀wal 1561   ∈ wcel 2145  ∀wral 3079

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1803  df-ral 3080

This theorem is referenced by:  r2ex  3202  r3al  3203  ralcom  3293  nfra2w  3301  moel  3390  raliunxp  5815  codir  6110  qfto  6111  dfpo2  6286  fununi  6600  dff13  7242  mpo2eqb  7532  frpoins3xpg  8124  xpord2indlem  8131  tz7.48lem  8416  qliftfun  8788  zorn2lem4  10471  isirred2  20491  isdomn3  20787  cnmpt12  23781  cnmpt22  23788  dchrelbas3  27356  ons2ind  28422  cvmlift2lem12  35672  dfso2  36113  r2alan  38757  inxpss  38823  inxpss3  38826  dfac5prim  45558  permac8prim  45582  iscnrm3lem2  49565  joindm2  49598  meetdm2  49600