Theorem r2al 3185

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 394  ∀wal 1532   ∈ wcel 2099  ∀wral 3051

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1775  df-ral 3052

This theorem is referenced by:  r2ex  3186  r3al  3187  ralcom  3277  nfra2w  3287  moel  3386  raliunxp  5846  codir  6132  qfto  6133  dfpo2  6307  fununi  6634  dff13  7270  mpo2eqb  7558  frpoins3xpg  8154  xpord2indlem  8161  tz7.48lem  8471  qliftfun  8831  zorn2lem4  10542  isirred2  20403  isdomn3  20693  cnmpt12  23662  cnmpt22  23669  dchrelbas3  27267  cvmlift2lem12  35142  dfso2  35577  r2alan  37947  inxpss  38009  inxpss3  38012  iscnrm3lem2  48268  joindm2  48302  meetdm2  48304