Theorem r2al 3201

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

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400  ∀wal 1568   ∈ wcel 2143  ∀wral 3079

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-ral 3080

This theorem is referenced by:  r2ex  3202  r3al  3203  ralcom  3293  nfra2w  3301  moel  3389  raliunxp  5827  codir  6122  qfto  6123  dfpo2  6299  fununi  6613  dff13  7254  mpo2eqb  7544  frpoins3xpg  8137  xpord2indlem  8144  tz7.48lem  8429  qliftfun  8801  zorn2lem4  10484  isirred2  20504  isdomn3  20800  cnmpt12  23805  cnmpt22  23812  dchrelbas3  27383  ons2ind  28449  cvmlift2lem12  35787  dfso2  36228  r2alan  38881  inxpss  38947  inxpss3  38950  dfac5prim  45682  permac8prim  45706  iscnrm3lem2  49696  joindm2  49729  meetdm2  49731