Theorem r2al 3199

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401  ∀wal 1568   ∈ wcel 2145  ∀wral 3077

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-ral 3078

This theorem is used by:  r2ex  3200  r3al  3201  ralcom  3291  nfra2w  3299  moel  3386  raliunxp  5816  codir  6112  qfto  6113  dfpo2  6292  fununi  6607  dff13  7250  mpo2eqb  7544  frpoins3xpg  8141  xpord2indlem  8148  tz7.48lemOLD  8435  qliftfun  8807  zorn2lem4  10558  isirred2  20631  isdomn3  20946  cnmpt12  23966  cnmpt22  23973  dchrelbas3  27547  ons2ind  28643  cvmlift2lem12  36048  dfso2  36489  r2alan  39151  inxpss  39217  inxpss3  39220  dfac5prim  45932  permac8prim  45956  iscnrm3lem2  49987  joindm2  50020  meetdm2  50022