![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > rspc2v | Structured version Visualization version GIF version |
Description: 2-variable restricted specialization, using implicit substitution. (Contributed by NM, 13-Sep-1999.) |
Ref | Expression |
---|---|
rspc2v.1 | ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜒)) |
rspc2v.2 | ⊢ (𝑦 = 𝐵 → (𝜒 ↔ 𝜓)) |
Ref | Expression |
---|---|
rspc2v | ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (∀𝑥 ∈ 𝐶 ∀𝑦 ∈ 𝐷 𝜑 → 𝜓)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | rspc2v.1 | . . . 4 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜒)) | |
2 | 1 | ralbidv 3164 | . . 3 ⊢ (𝑥 = 𝐴 → (∀𝑦 ∈ 𝐷 𝜑 ↔ ∀𝑦 ∈ 𝐷 𝜒)) |
3 | 2 | rspcv 3555 | . 2 ⊢ (𝐴 ∈ 𝐶 → (∀𝑥 ∈ 𝐶 ∀𝑦 ∈ 𝐷 𝜑 → ∀𝑦 ∈ 𝐷 𝜒)) |
4 | rspc2v.2 | . . 3 ⊢ (𝑦 = 𝐵 → (𝜒 ↔ 𝜓)) | |
5 | 4 | rspcv 3555 | . 2 ⊢ (𝐵 ∈ 𝐷 → (∀𝑦 ∈ 𝐷 𝜒 → 𝜓)) |
6 | 3, 5 | sylan9 508 | 1 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (∀𝑥 ∈ 𝐶 ∀𝑦 ∈ 𝐷 𝜑 → 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 207 ∧ wa 396 = wceq 1522 ∈ wcel 2081 ∀wral 3105 |
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-ext 2769 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 843 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-v 3439 |
This theorem is referenced by: rspc2va 3573 rspc3v 3575 disji2 4946 f1veqaeq 6880 isorel 6942 isosolem 6963 oveqrspc2v 7043 fovcl 7135 caovclg 7196 caovcomg 7199 smoel 7849 fiint 8641 dffi3 8741 ltordlem 11013 seqhomo 13267 cshf1 14008 climcn2 14783 drsdir 17374 tsrlin 17658 dirge 17676 mhmlin 17781 issubg2 18048 nsgbi 18064 ghmlin 18104 efgi 18572 efgred 18601 irredmul 19149 issubrg2 19245 abvmul 19290 abvtri 19291 lmodlema 19329 islmodd 19330 rmodislmodlem 19391 rmodislmod 19392 lmhmlin 19497 lbsind 19542 mplcoe5lem 19935 ipcj 20460 obsip 20547 matecl 20718 dmatelnd 20789 scmateALT 20805 mdetdiaglem 20891 mdetdiagid 20893 pmatcoe1fsupp 20993 m2cpminvid2lem 21046 inopn 21191 basis1 21242 basis2 21243 iscldtop 21387 hausnei 21620 t1sep2 21661 nconnsubb 21715 r0sep 22040 fbasssin 22128 fcfneii 22329 ustssel 22497 xmeteq0 22631 tngngp3 22948 nmvs 22968 cncfi 23185 c1lip1 24277 aalioulem3 24606 logltb 24864 cvxcl 25244 2sqlem8 25684 axtgcgrrflx 25930 axtgsegcon 25932 axtg5seg 25933 axtgbtwnid 25934 axtgpasch 25935 axtgcont1 25936 axtgupdim2 25939 axtgeucl 25940 isperp2d 26184 f1otrgds 26338 brbtwn2 26374 axcontlem3 26435 axcontlem9 26441 axcontlem10 26442 upgrwlkdvdelem 27204 conngrv2edg 27661 frgrwopreglem5ALT 27793 ablocom 28016 nvs 28131 nvtri 28138 phpar2 28291 phpar 28292 shaddcl 28685 shmulcl 28686 cnopc 29381 unop 29383 hmop 29390 cnfnc 29398 adj1 29401 hstel2 29687 stj 29703 stcltr1i 29742 mddmdin0i 29899 cdj3lem1 29902 cdj3lem2b 29905 disji2f 30017 disjif2 30021 disjxpin 30028 fovcld 30075 isoun 30125 archirng 30455 archiexdiv 30457 slmdlema 30469 inelcarsg 31186 sibfof 31215 breprexplema 31518 axtgupdim2ALTV 31556 pconncn 32079 nocvxminlem 32856 ivthALT 33292 poimirlem32 34455 ismtycnv 34612 ismtyima 34613 ismtyres 34618 bfplem1 34632 bfplem2 34633 ghomlinOLD 34698 rngohomadd 34779 rngohommul 34780 crngocom 34811 idladdcl 34829 idllmulcl 34830 idlrmulcl 34831 pridl 34847 ispridlc 34880 pridlc 34881 dmnnzd 34885 oposlem 35849 omllaw 35910 hlsuprexch 36048 lautle 36751 ltrnu 36788 tendovalco 37432 ntrkbimka 39873 mullimc 41439 mullimcf 41446 lptre2pt 41463 fourierdlem54 41987 faovcl 42915 icceuelpartlem 43077 iccpartnel 43080 fargshiftf1 43083 sprsymrelfolem2 43137 reuopreuprim 43170 mgmhmlin 43535 issubmgm2 43539 |
Copyright terms: Public domain | W3C validator |