![]() |
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 5709 | . . 3 ⊢ ∪ 𝑦 ∈ 𝐴 ({𝑦} × 𝐵) = (𝐴 × 𝐵) | |
2 | 1 | raleqi 3314 | . 2 ⊢ (∀𝑥 ∈ ∪ 𝑦 ∈ 𝐴 ({𝑦} × 𝐵)𝜑 ↔ ∀𝑥 ∈ (𝐴 × 𝐵)𝜑) |
3 | ralxp.1 | . . 3 ⊢ (𝑥 = ⟨𝑦, 𝑧⟩ → (𝜑 ↔ 𝜓)) | |
4 | 3 | raliunxp 5800 | . 2 ⊢ (∀𝑥 ∈ ∪ 𝑦 ∈ 𝐴 ({𝑦} × 𝐵)𝜑 ↔ ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐵 𝜓) |
5 | 2, 4 | bitr3i 277 | 1 ⊢ (∀𝑥 ∈ (𝐴 × 𝐵)𝜑 ↔ ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐵 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 = wceq 1542 ∀wral 3065 {csn 4591 ⟨cop 4597 ∪ ciun 4959 × cxp 5636 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-10 2138 ax-11 2155 ax-12 2172 ax-ext 2708 ax-sep 5261 ax-nul 5268 ax-pr 5389 |
This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1783 df-nf 1787 df-sb 2069 df-clab 2715 df-cleq 2729 df-clel 2815 df-nfc 2890 df-ral 3066 df-rex 3075 df-rab 3411 df-v 3450 df-sbc 3745 df-csb 3861 df-dif 3918 df-un 3920 df-in 3922 df-ss 3932 df-nul 4288 df-if 4492 df-sn 4592 df-pr 4594 df-op 4598 df-iun 4961 df-opab 5173 df-xp 5644 df-rel 5645 |
This theorem is referenced by: ralxpf 5807 reu3op 6249 f1opr 7418 ffnov 7488 eqfnov 7490 funimassov 7536 f1stres 7950 f2ndres 7951 naddf 8632 ecopover 8767 xpf1o 9090 xpwdomg 9528 rankxplim 9822 imasaddfnlem 17417 imasvscafn 17426 comfeq 17593 isssc 17710 isfuncd 17758 cofucl 17781 funcres2b 17790 evlfcl 18118 uncfcurf 18135 yonedalem3 18176 yonedainv 18177 efgval2 19513 srgfcl 19934 txbas 22934 hausdiag 23012 tx1stc 23017 txkgen 23019 xkococn 23027 cnmpt21 23038 xkoinjcn 23054 tmdcn2 23456 clssubg 23476 qustgplem 23488 txmetcnp 23919 txmetcn 23920 qtopbaslem 24138 bndth 24337 cxpcn3 26117 dvdsmulf1o 26559 fsumdvdsmul 26560 addsf 27314 xrofsup 31714 txpconn 33866 cvmlift2lem1 33936 cvmlift2lem12 33948 mclsax 34203 ismtyhmeolem 36292 dih1dimatlem 39821 ffnaov 45505 ovn0ssdmfun 46135 plusfreseq 46140 funcf2lem 47112 |
Copyright terms: Public domain | W3C validator |