Theorem r2al 3202

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

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

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 1945

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

This theorem is used by:  r2ex  3203  r3al  3204  ralcom  3294  nfra2w  3302  moel  3389  raliunxp  5823  codir  6127  qfto  6128  dfpo2  6320  fununi  6640  dff13  7284  mpo2eqb  7578  frpoins3xpg  8187  xpord2indlem  8194  tz7.48lemOLD  8482  qliftfun  8854  zorn2lem4  10607  isirred2  20684  isdomn3  20999  cnmpt12  24019  cnmpt22  24026  dchrelbas3  27598  ons2ind  28694  cvmlift2lem12  36259  dfso2  36711  r2alan  39386  inxpss  39452  inxpss3  39455  dfac5prim  46186  permac8prim  46210  iscnrm3lem2  50264  joindm2  50297  meetdm2  50299