Theorem r2al 3165

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 3117	1 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 ↔ ∀𝑥∀𝑦((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝜑))

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

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 3045

This theorem is referenced by:  r2ex  3166  r3al  3167  ralcom  3257  nfra2w  3266  moel  3367  raliunxp  5786  codir  6073  qfto  6074  dfpo2  6248  fununi  6561  dff13  7195  mpo2eqb  7485  frpoins3xpg  8080  xpord2indlem  8087  tz7.48lem  8370  qliftfun  8736  zorn2lem4  10412  isirred2  20324  isdomn3  20618  cnmpt12  23570  cnmpt22  23577  dchrelbas3  27165  cvmlift2lem12  35286  dfso2  35727  r2alan  38223  inxpss  38284  inxpss3  38287  dfac5prim  44964  permac8prim  44988  iscnrm3lem2  48920  joindm2  48953  meetdm2  48955