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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395  ∀wal 1540   ∈ wcel 2114  ∀wral 3052

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-ral 3053

This theorem is referenced by:  r2ex  3175  r3al  3176  ralcom  3266  nfra2w  3274  moel  3363  raliunxp  5788  codir  6077  qfto  6078  dfpo2  6254  fununi  6567  dff13  7202  mpo2eqb  7492  frpoins3xpg  8083  xpord2indlem  8090  tz7.48lem  8373  qliftfun  8742  zorn2lem4  10412  isirred2  20392  isdomn3  20683  cnmpt12  23642  cnmpt22  23649  dchrelbas3  27215  ons2ind  28281  cvmlift2lem12  35512  dfso2  35953  r2alan  38586  inxpss  38652  inxpss3  38655  dfac5prim  45435  permac8prim  45459  iscnrm3lem2  49422  joindm2  49455  meetdm2  49457