Theorem r2al 3181

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910

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

This theorem is referenced by:  r2ex  3182  r3al  3183  ralcom  3274  nfra2w  3284  moel  3386  raliunxp  5824  codir  6114  qfto  6115  dfpo2  6290  fununi  6616  dff13  7252  mpo2eqb  7544  frpoins3xpg  8144  xpord2indlem  8151  tz7.48lem  8460  qliftfun  8821  zorn2lem4  10518  isirred2  20386  isdomn3  20680  cnmpt12  23610  cnmpt22  23617  dchrelbas3  27206  cvmlift2lem12  35341  dfso2  35777  r2alan  38272  inxpss  38334  inxpss3  38337  dfac5prim  44982  iscnrm3lem2  48876  joindm2  48909  meetdm2  48911