Theorem r2al 3176

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

Syntax hints:   → wi 4   ↔ wb 207   ∧ wa 396  ∀wal 1545   ∈ wcel 2119  ∀wral 3054

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-ral 3055

This theorem is referenced by:  r2ex  3177  r3al  3178  ralcom  3268  nfra2w  3276  moel  3365  raliunxp  5788  codir  6077  qfto  6078  dfpo2  6254  fununi  6567  dff13  7205  mpo2eqb  7495  frpoins3xpg  8087  xpord2indlem  8094  tz7.48lem  8377  qliftfun  8746  zorn2lem4  10419  isirred2  20399  isdomn3  20694  cnmpt12  23657  cnmpt22  23664  dchrelbas3  27226  ons2ind  28292  cvmlift2lem12  35549  dfso2  35990  r2alan  38625  inxpss  38691  inxpss3  38694  dfac5prim  45441  permac8prim  45465  iscnrm3lem2  49432  joindm2  49465  meetdm2  49467