Theorem r2al 3172

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

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

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 3052

This theorem is referenced by:  r2ex  3173  r3al  3174  ralcom  3264  nfra2w  3272  moel  3370  raliunxp  5788  codir  6077  qfto  6078  dfpo2  6254  fununi  6567  dff13  7200  mpo2eqb  7490  frpoins3xpg  8082  xpord2indlem  8089  tz7.48lem  8372  qliftfun  8739  zorn2lem4  10409  isirred2  20357  isdomn3  20648  cnmpt12  23611  cnmpt22  23618  dchrelbas3  27205  ons2ind  28271  cvmlift2lem12  35508  dfso2  35949  r2alan  38443  inxpss  38506  inxpss3  38509  dfac5prim  45227  permac8prim  45251  iscnrm3lem2  49176  joindm2  49209  meetdm2  49211