Theorem ralxp 5829

Description: Universal quantification restricted to a Cartesian product is equivalent to a double restricted quantification. The hypothesis specifies an implicit substitution. (Contributed by NM, 7-Feb-2004.) (Revised by Mario Carneiro, 29-Dec-2014.)

Hypothesis

Ref	Expression
ralxp.1	⊢ (𝑥 = ⟨𝑦, 𝑧⟩ → (𝜑 ↔ 𝜓))

Assertion

Ref	Expression
ralxp	⊢ (∀𝑥 ∈ (𝐴 × 𝐵)𝜑 ↔ ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐵 𝜓)

Distinct variable groups:   𝑥,𝑦,𝑧,𝐴   𝑥,𝐵,𝑧   𝜑,𝑦,𝑧   𝜓,𝑥   𝑦,𝐵

Allowed substitution hints:   𝜑(𝑥)   𝜓(𝑦,𝑧)

Proof of Theorem ralxp

Step	Hyp	Ref	Expression
1		iunxpconst 5736	. . 3 ⊢ ∪ 𝑦 ∈ 𝐴 ({𝑦} × 𝐵) = (𝐴 × 𝐵)
2	1	raleqi 3321	. 2 ⊢ (∀𝑥 ∈ ∪ 𝑦 ∈ 𝐴 ({𝑦} × 𝐵)𝜑 ↔ ∀𝑥 ∈ (𝐴 × 𝐵)𝜑)
3		ralxp.1	. . 3 ⊢ (𝑥 = ⟨𝑦, 𝑧⟩ → (𝜑 ↔ 𝜓))
4	3	raliunxp 5827	. 2 ⊢ (∀𝑥 ∈ ∪ 𝑦 ∈ 𝐴 ({𝑦} × 𝐵)𝜑 ↔ ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐵 𝜓)
5	2, 4	bitr3i 280	1 ⊢ (∀𝑥 ∈ (𝐴 × 𝐵)𝜑 ↔ ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐵 𝜓)

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1570  ∀wral 3079  {csn 4590  ⟨cop 4596  ∪ ciun 4957   × cxp 5661

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-sep 5258  ax-pr 5406

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-sbc 3746  df-csb 3855  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4288  df-if 4489  df-sn 4591  df-pr 4593  df-op 4597  df-iun 4959  df-opab 5175  df-xp 5669  df-rel 5670

This theorem is referenced by:  ralxpf  5834  reu3op  6295  f1opr  7468  ffnov  7538  eqfnov  7541  funimassov  7589  f1stres  8011  f2ndres  8012  naddf  8669  ecopover  8820  xpf1o  9128  xpwdomg  9548  rankxplim  9852  imasaddfnlem  17583  imasvscafn  17592  comfeq  17763  isssc  17878  isfuncd  17923  cofucl  17946  funcres2b  17955  evlfcl  18279  uncfcurf  18296  yonedalem3  18337  yonedainv  18338  efgval2  19795  srgfcl  20279  txbas  23705  hausdiag  23783  tx1stc  23788  txkgen  23790  xkococn  23798  cnmpt21  23809  xkoinjcn  23825  tmdcn2  24227  clssubg  24247  qustgplem  24259  txmetcnp  24685  txmetcn  24686  qtopbaslem  24896  bndth  25098  cxpcn3  26894  mpodvdsmulf1o  27339  fsumdvdsmul  27340  dvdsmulf1o  27341  addsf  28156  xrofsup  33093  txpconn  35705  cvmlift2lem1  35775  cvmlift2lem12  35787  mclsax  36042  ismtyhmeolem  38436  dih1dimatlem  42084  ffnaov  47919  ovn0ssdmfun  48907  plusfreseq  48912  funcf2lem  49842  imaidfu  49871  imasubc  49912  imassc  49914  fucofulem2  50072