![]() |
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 5515 | . . 3 ⊢ ∪ 𝑦 ∈ 𝐴 ({𝑦} × 𝐵) = (𝐴 × 𝐵) | |
2 | 1 | raleqi 3373 | . 2 ⊢ (∀𝑥 ∈ ∪ 𝑦 ∈ 𝐴 ({𝑦} × 𝐵)𝜑 ↔ ∀𝑥 ∈ (𝐴 × 𝐵)𝜑) |
3 | ralxp.1 | . . 3 ⊢ (𝑥 = 〈𝑦, 𝑧〉 → (𝜑 ↔ 𝜓)) | |
4 | 3 | raliunxp 5601 | . 2 ⊢ (∀𝑥 ∈ ∪ 𝑦 ∈ 𝐴 ({𝑦} × 𝐵)𝜑 ↔ ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐵 𝜓) |
5 | 2, 4 | bitr3i 278 | 1 ⊢ (∀𝑥 ∈ (𝐴 × 𝐵)𝜑 ↔ ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐵 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 207 = wceq 1522 ∀wral 3105 {csn 4476 〈cop 4482 ∪ ciun 4829 × cxp 5446 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1777 ax-4 1791 ax-5 1888 ax-6 1947 ax-7 1992 ax-8 2083 ax-9 2091 ax-10 2112 ax-11 2126 ax-12 2141 ax-13 2344 ax-ext 2769 ax-sep 5099 ax-nul 5106 ax-pr 5226 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 843 df-3an 1082 df-tru 1525 df-ex 1762 df-nf 1766 df-sb 2043 df-clab 2776 df-cleq 2788 df-clel 2863 df-nfc 2935 df-ral 3110 df-rex 3111 df-rab 3114 df-v 3439 df-sbc 3710 df-csb 3816 df-dif 3866 df-un 3868 df-in 3870 df-ss 3878 df-nul 4216 df-if 4386 df-sn 4477 df-pr 4479 df-op 4483 df-iun 4831 df-opab 5029 df-xp 5454 df-rel 5455 |
This theorem is referenced by: ralxpf 5608 reu3op 6023 f1opr 7074 ffnov 7139 eqfnov 7141 funimassov 7186 f1stres 7574 f2ndres 7575 ecopover 8256 xpf1o 8531 xpwdomg 8900 rankxplim 9159 imasaddfnlem 16635 imasvscafn 16644 comfeq 16810 isssc 16924 isfuncd 16969 cofucl 16992 funcres2b 17001 evlfcl 17306 uncfcurf 17323 yonedalem3 17364 yonedainv 17365 efgval2 18582 srgfcl 18960 txbas 21864 hausdiag 21942 tx1stc 21947 txkgen 21949 xkococn 21957 cnmpt21 21968 xkoinjcn 21984 tmdcn2 22386 clssubg 22405 qustgplem 22417 txmetcnp 22845 txmetcn 22846 qtopbaslem 23055 bndth 23250 cxpcn3 25015 dvdsmulf1o 25458 fsumdvdsmul 25459 xrofsup 30185 txpconn 32094 cvmlift2lem1 32164 cvmlift2lem12 32176 mclsax 32431 ismtyhmeolem 34640 dih1dimatlem 38022 ffnaov 42941 ovn0ssdmfun 43543 plusfreseq 43548 |
Copyright terms: Public domain | W3C validator |