![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > rspc2v | 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 | nfv 1539 | . 2 ⊢ Ⅎ𝑥𝜒 | |
2 | nfv 1539 | . 2 ⊢ Ⅎ𝑦𝜓 | |
3 | rspc2v.1 | . 2 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜒)) | |
4 | rspc2v.2 | . 2 ⊢ (𝑦 = 𝐵 → (𝜒 ↔ 𝜓)) | |
5 | 1, 2, 3, 4 | rspc2 2867 | 1 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (∀𝑥 ∈ 𝐶 ∀𝑦 ∈ 𝐷 𝜑 → 𝜓)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 104 ↔ wb 105 = wceq 1364 ∈ wcel 2160 ∀wral 2468 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-io 710 ax-5 1458 ax-7 1459 ax-gen 1460 ax-ie1 1504 ax-ie2 1505 ax-8 1515 ax-10 1516 ax-11 1517 ax-i12 1518 ax-bndl 1520 ax-4 1521 ax-17 1537 ax-i9 1541 ax-ial 1545 ax-i5r 1546 ax-ext 2171 |
This theorem depends on definitions: df-bi 117 df-tru 1367 df-nf 1472 df-sb 1774 df-clab 2176 df-cleq 2182 df-clel 2185 df-nfc 2321 df-ral 2473 df-v 2754 |
This theorem is referenced by: rspc2va 2870 rspc3v 2872 disji2 4011 ontriexmidim 4536 wetriext 4591 f1veqaeq 5786 isorel 5825 oveqrspc2v 5918 fovcld 5996 caovclg 6044 caovcomg 6047 smoel 6319 dcdifsnid 6523 unfiexmid 6935 fiintim 6946 supmoti 7010 supsnti 7022 isotilem 7023 onntri35 7254 onntri45 7258 cauappcvgprlem1 7676 caucvgprlemnkj 7683 caucvgprlemnbj 7684 caucvgprprlemval 7705 ltordlem 8457 frecuzrdgrrn 10426 frec2uzrdg 10427 frecuzrdgrcl 10428 frecuzrdgrclt 10433 seq3caopr3 10499 seq3homo 10528 climcn2 11335 fprodcl2lem 11631 ennnfonelemim 12443 mhmlin 12885 issubg2m 13094 nsgbi 13109 ghmlin 13148 issubrng2 13518 issubrg2 13549 lmodlema 13569 islmodd 13570 rmodislmodlem 13627 rmodislmod 13628 rnglidlmcl 13757 inopn 13900 basis1 13944 basis2 13945 xmeteq0 14256 cncfi 14462 limccnp2lem 14542 logltb 14692 2sqlem8 14867 redcwlpo 15201 redc0 15203 reap0 15204 |
Copyright terms: Public domain | W3C validator |