Theorem r2al 3174

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

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

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 3053

This theorem is referenced by:  r2ex  3175  r3al  3176  ralcom  3266  nfra2w  3274  moel  3372  raliunxp  5796  codir  6085  qfto  6086  dfpo2  6262  fununi  6575  dff13  7210  mpo2eqb  7500  frpoins3xpg  8092  xpord2indlem  8099  tz7.48lem  8382  qliftfun  8751  zorn2lem4  10421  isirred2  20369  isdomn3  20660  cnmpt12  23623  cnmpt22  23630  dchrelbas3  27217  ons2ind  28283  cvmlift2lem12  35527  dfso2  35968  r2alan  38496  inxpss  38562  inxpss3  38565  dfac5prim  45340  permac8prim  45364  iscnrm3lem2  49288  joindm2  49321  meetdm2  49323