Theorem r2al 3168

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395  ∀wal 1539   ∈ wcel 2111  ∀wral 3047

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-ral 3048

This theorem is referenced by:  r2ex  3169  r3al  3170  ralcom  3260  nfra2w  3268  moel  3366  raliunxp  5779  codir  6067  qfto  6068  dfpo2  6243  fununi  6556  dff13  7188  mpo2eqb  7478  frpoins3xpg  8070  xpord2indlem  8077  tz7.48lem  8360  qliftfun  8726  zorn2lem4  10387  isirred2  20337  isdomn3  20628  cnmpt12  23580  cnmpt22  23587  dchrelbas3  27174  cvmlift2lem12  35346  dfso2  35787  r2alan  38283  inxpss  38344  inxpss3  38347  dfac5prim  45022  permac8prim  45046  iscnrm3lem2  48965  joindm2  48998  meetdm2  49000