Theorem r2al 3195

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395  ∀wal 1538   ∈ wcel 2108  ∀wral 3061

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-ral 3062

This theorem is referenced by:  r2ex  3196  r3al  3197  ralcom  3289  nfra2w  3299  moel  3402  raliunxp  5850  codir  6140  qfto  6141  dfpo2  6316  fununi  6641  dff13  7275  mpo2eqb  7565  frpoins3xpg  8165  xpord2indlem  8172  tz7.48lem  8481  qliftfun  8842  zorn2lem4  10539  isirred2  20421  isdomn3  20715  cnmpt12  23675  cnmpt22  23682  dchrelbas3  27282  cvmlift2lem12  35319  dfso2  35755  r2alan  38250  inxpss  38312  inxpss3  38315  dfac5prim  45007  iscnrm3lem2  48832  joindm2  48865  meetdm2  48867