Theorem r2al 3173

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

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

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 3052

This theorem is referenced by:  r2ex  3174  r3al  3175  ralcom  3265  nfra2w  3273  moel  3362  raliunxp  5794  codir  6083  qfto  6084  dfpo2  6260  fununi  6573  dff13  7209  mpo2eqb  7499  frpoins3xpg  8090  xpord2indlem  8097  tz7.48lem  8380  qliftfun  8749  zorn2lem4  10421  isirred2  20401  isdomn3  20692  cnmpt12  23632  cnmpt22  23639  dchrelbas3  27201  ons2ind  28267  cvmlift2lem12  35496  dfso2  35937  r2alan  38572  inxpss  38638  inxpss3  38641  dfac5prim  45417  permac8prim  45441  iscnrm3lem2  49410  joindm2  49443  meetdm2  49445