Theorem ralxp 5866

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 5772	. . 3 ⊢ ∪ 𝑦 ∈ 𝐴 ({𝑦} × 𝐵) = (𝐴 × 𝐵)
2	1	raleqi 3332	. 2 ⊢ (∀𝑥 ∈ ∪ 𝑦 ∈ 𝐴 ({𝑦} × 𝐵)𝜑 ↔ ∀𝑥 ∈ (𝐴 × 𝐵)𝜑)
3		ralxp.1	. . 3 ⊢ (𝑥 = ⟨𝑦, 𝑧⟩ → (𝜑 ↔ 𝜓))
4	3	raliunxp 5864	. 2 ⊢ (∀𝑥 ∈ ∪ 𝑦 ∈ 𝐴 ({𝑦} × 𝐵)𝜑 ↔ ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐵 𝜓)
5	2, 4	bitr3i 277	1 ⊢ (∀𝑥 ∈ (𝐴 × 𝐵)𝜑 ↔ ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐵 𝜓)

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1537  ∀wral 3067  {csn 4648  ⟨cop 4654  ∪ ciun 5015   × cxp 5698

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711  ax-sep 5317  ax-nul 5324  ax-pr 5447

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-nfc 2895  df-ral 3068  df-rex 3077  df-rab 3444  df-v 3490  df-sbc 3805  df-csb 3922  df-dif 3979  df-un 3981  df-ss 3993  df-nul 4353  df-if 4549  df-sn 4649  df-pr 4651  df-op 4655  df-iun 5017  df-opab 5229  df-xp 5706  df-rel 5707

This theorem is referenced by:  ralxpf  5871  reu3op  6323  f1opr  7506  ffnov  7576  eqfnov  7579  funimassov  7627  f1stres  8054  f2ndres  8055  naddf  8737  ecopover  8879  xpf1o  9205  xpwdomg  9654  rankxplim  9948  imasaddfnlem  17588  imasvscafn  17597  comfeq  17764  isssc  17881  isfuncd  17929  cofucl  17952  funcres2b  17961  evlfcl  18292  uncfcurf  18309  yonedalem3  18350  yonedainv  18351  efgval2  19766  srgfcl  20223  txbas  23596  hausdiag  23674  tx1stc  23679  txkgen  23681  xkococn  23689  cnmpt21  23700  xkoinjcn  23716  tmdcn2  24118  clssubg  24138  qustgplem  24150  txmetcnp  24581  txmetcn  24582  qtopbaslem  24800  bndth  25009  cxpcn3  26809  mpodvdsmulf1o  27255  fsumdvdsmul  27256  dvdsmulf1o  27257  fsumdvdsmulOLD  27258  addsf  28033  xrofsup  32774  txpconn  35200  cvmlift2lem1  35270  cvmlift2lem12  35282  mclsax  35537  ismtyhmeolem  37764  dih1dimatlem  41286  ffnaov  47114  ovn0ssdmfun  47882  plusfreseq  47887  funcf2lem  48685