![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > ralxp | Structured version Visualization version GIF version |
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.) |
Ref | Expression |
---|---|
ralxp.1 | ⊢ (𝑥 = 〈𝑦, 𝑧〉 → (𝜑 ↔ 𝜓)) |
Ref | Expression |
---|---|
ralxp | ⊢ (∀𝑥 ∈ (𝐴 × 𝐵)𝜑 ↔ ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐵 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | iunxpconst 5750 | . . 3 ⊢ ∪ 𝑦 ∈ 𝐴 ({𝑦} × 𝐵) = (𝐴 × 𝐵) | |
2 | 1 | raleqi 3312 | . 2 ⊢ (∀𝑥 ∈ ∪ 𝑦 ∈ 𝐴 ({𝑦} × 𝐵)𝜑 ↔ ∀𝑥 ∈ (𝐴 × 𝐵)𝜑) |
3 | ralxp.1 | . . 3 ⊢ (𝑥 = 〈𝑦, 𝑧〉 → (𝜑 ↔ 𝜓)) | |
4 | 3 | raliunxp 5842 | . 2 ⊢ (∀𝑥 ∈ ∪ 𝑦 ∈ 𝐴 ({𝑦} × 𝐵)𝜑 ↔ ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐵 𝜓) |
5 | 2, 4 | bitr3i 276 | 1 ⊢ (∀𝑥 ∈ (𝐴 × 𝐵)𝜑 ↔ ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐵 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 = wceq 1533 ∀wral 3050 {csn 4630 〈cop 4636 ∪ ciun 4997 × cxp 5676 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-10 2129 ax-11 2146 ax-12 2166 ax-ext 2696 ax-sep 5300 ax-nul 5307 ax-pr 5429 |
This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 df-3an 1086 df-tru 1536 df-fal 1546 df-ex 1774 df-nf 1778 df-sb 2060 df-clab 2703 df-cleq 2717 df-clel 2802 df-nfc 2877 df-ral 3051 df-rex 3060 df-rab 3419 df-v 3463 df-sbc 3774 df-csb 3890 df-dif 3947 df-un 3949 df-ss 3961 df-nul 4323 df-if 4531 df-sn 4631 df-pr 4633 df-op 4637 df-iun 4999 df-opab 5212 df-xp 5684 df-rel 5685 |
This theorem is referenced by: ralxpf 5849 reu3op 6298 f1opr 7476 ffnov 7547 eqfnov 7550 funimassov 7598 f1stres 8018 f2ndres 8019 naddf 8702 ecopover 8840 xpf1o 9164 xpwdomg 9610 rankxplim 9904 imasaddfnlem 17513 imasvscafn 17522 comfeq 17689 isssc 17806 isfuncd 17854 cofucl 17877 funcres2b 17886 evlfcl 18217 uncfcurf 18234 yonedalem3 18275 yonedainv 18276 efgval2 19691 srgfcl 20148 txbas 23515 hausdiag 23593 tx1stc 23598 txkgen 23600 xkococn 23608 cnmpt21 23619 xkoinjcn 23635 tmdcn2 24037 clssubg 24057 qustgplem 24069 txmetcnp 24500 txmetcn 24501 qtopbaslem 24719 bndth 24928 cxpcn3 26728 mpodvdsmulf1o 27171 fsumdvdsmul 27172 dvdsmulf1o 27173 fsumdvdsmulOLD 27174 addsf 27945 xrofsup 32619 txpconn 34973 cvmlift2lem1 35043 cvmlift2lem12 35055 mclsax 35310 ismtyhmeolem 37408 dih1dimatlem 40932 ffnaov 46717 ovn0ssdmfun 47407 plusfreseq 47412 funcf2lem 48210 |
Copyright terms: Public domain | W3C validator |