Theorem r2al 3198

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401  ∀wal 1567   ∈ wcel 2144  ∀wral 3076

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-ral 3077

This theorem is used by:  r2ex  3199  r3al  3200  ralcom  3290  nfra2w  3298  moel  3385  raliunxp  5815  codir  6113  qfto  6114  dfpo2  6299  fununi  6616  dff13  7259  mpo2eqb  7553  frpoins3xpg  8160  xpord2indlem  8167  tz7.48lemOLD  8455  qliftfun  8827  zorn2lem4  10581  isirred2  20657  isdomn3  20972  cnmpt12  23992  cnmpt22  23999  dchrelbas3  27571  ons2ind  28667  cvmlift2lem12  36166  dfso2  36613  r2alan  39277  inxpss  39343  inxpss3  39346  dfac5prim  46074  permac8prim  46098  iscnrm3lem2  50143  joindm2  50176  meetdm2  50178