Theorem r2al 3204

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

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

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 3083

This theorem is used by:  r2ex  3205  r3al  3206  ralcom  3296  nfra2w  3304  moel  3392  raliunxp  5830  codir  6125  qfto  6126  dfpo2  6304  fununi  6618  dff13  7259  mpo2eqb  7555  frpoins3xpg  8145  xpord2indlem  8152  tz7.48lem  8437  qliftfun  8809  zorn2lem4  10501  isirred2  20536  isdomn3  20850  cnmpt12  23861  cnmpt22  23868  dchrelbas3  27439  ons2ind  28505  cvmlift2lem12  35827  dfso2  36268  r2alan  38941  inxpss  39007  inxpss3  39010  dfac5prim  45740  permac8prim  45764  iscnrm3lem2  49754  joindm2  49787  meetdm2  49789