Theorem r2al 3177

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

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 397  ∀wal 1546   ∈ wcel 2121  ∀wral 3055

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918

This theorem depends on definitions:  df-bi 209  df-an 398  df-ex 1788  df-ral 3056

This theorem is referenced by:  r2ex  3178  r3al  3179  ralcom  3269  nfra2w  3277  moel  3366  raliunxp  5784  codir  6077  qfto  6078  dfpo2  6251  fununi  6564  dff13  7202  mpo2eqb  7492  frpoins3xpg  8084  xpord2indlem  8091  tz7.48lem  8374  qliftfun  8743  zorn2lem4  10416  isirred2  20396  isdomn3  20691  cnmpt12  23654  cnmpt22  23661  dchrelbas3  27223  ons2ind  28289  cvmlift2lem12  35557  dfso2  35998  r2alan  38633  inxpss  38699  inxpss3  38702  dfac5prim  45449  permac8prim  45473  iscnrm3lem2  49439  joindm2  49472  meetdm2  49474