Theorem r2al 3197

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

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 399  ∀wal 1557   ∈ wcel 2141  ∀wral 3075

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1799  df-ral 3076

This theorem is referenced by:  r2ex  3198  r3al  3199  ralcom  3289  nfra2w  3297  moel  3386  raliunxp  5807  codir  6102  qfto  6103  dfpo2  6277  fununi  6590  dff13  7232  mpo2eqb  7522  frpoins3xpg  8113  xpord2indlem  8120  tz7.48lem  8405  qliftfun  8777  zorn2lem4  10449  isirred2  20456  isdomn3  20751  cnmpt12  23714  cnmpt22  23721  dchrelbas3  27289  ons2ind  28355  cvmlift2lem12  35624  dfso2  36065  r2alan  38710  inxpss  38776  inxpss3  38779  dfac5prim  45526  permac8prim  45550  iscnrm3lem2  49516  joindm2  49549  meetdm2  49551