![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > rspc2va | Structured version Visualization version GIF version |
Description: 2-variable restricted specialization, using implicit substitution. (Contributed by NM, 18-Jun-2014.) |
Ref | Expression |
---|---|
rspc2v.1 | ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜒)) |
rspc2v.2 | ⊢ (𝑦 = 𝐵 → (𝜒 ↔ 𝜓)) |
Ref | Expression |
---|---|
rspc2va | ⊢ (((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) ∧ ∀𝑥 ∈ 𝐶 ∀𝑦 ∈ 𝐷 𝜑) → 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | rspc2v.1 | . . 3 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜒)) | |
2 | rspc2v.2 | . . 3 ⊢ (𝑦 = 𝐵 → (𝜒 ↔ 𝜓)) | |
3 | 1, 2 | rspc2v 3620 | . 2 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (∀𝑥 ∈ 𝐶 ∀𝑦 ∈ 𝐷 𝜑 → 𝜓)) |
4 | 3 | imp 408 | 1 ⊢ (((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) ∧ ∀𝑥 ∈ 𝐶 ∀𝑦 ∈ 𝐷 𝜑) → 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∧ wa 397 = wceq 1542 ∈ wcel 2107 ∀wral 3062 |
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-ext 2704 |
This theorem depends on definitions: df-bi 206 df-an 398 df-tru 1545 df-ex 1783 df-sb 2069 df-clab 2711 df-cleq 2725 df-clel 2811 df-ral 3063 |
This theorem is referenced by: rspc2dv 3624 swopo 5597 soisores 7318 soisoi 7319 isocnv 7321 isotr 7327 ovrspc2v 7429 caofrss 7700 caonncan 7705 frpoins3xpg 8120 coflton 8665 wunpr 10699 injresinj 13748 seqcaopr2 13999 rlimcn3 15529 o1of2 15552 isprm6 16646 ssc2 17764 pospropd 18275 tleile 18369 mhmpropd 18673 grpidssd 18894 grpinvssd 18895 dfgrp3lem 18916 isnsg3 19033 cyccom 19073 symgextf1 19281 efgredlemd 19604 efgredlem 19607 rglcom4d 20024 issrngd 20456 domneq0 20899 lindfind 21354 lindsind 21355 mplsubglem 21539 mdetunilem1 22095 mdetunilem3 22097 mdetunilem4 22098 mdetunilem9 22103 decpmatmulsumfsupp 22256 pm2mpf1 22282 pm2mpmhmlem1 22301 t0sep 22809 tsmsxplem2 23639 comet 24003 nrmmetd 24064 tngngp 24152 reconnlem2 24324 iscmet3lem1 24789 iscmet3lem2 24790 dchrisumlem1 26971 pntpbnd1 27068 ssltsepc 27273 tgjustc1 27705 tgjustc2 27706 iscgrglt 27744 motcgr 27766 perpneq 27944 foot 27952 f1otrg 28101 axcontlem10 28210 frgr2wwlk1 29561 orngmul 32389 lindsunlem 32653 mndpluscn 32843 unelros 33106 difelros 33107 inelsros 33113 diffiunisros 33114 cvxsconn 34171 elmrsubrn 34448 ghomco 36696 sticksstones10 40908 sticksstones12a 40910 fsuppind 41111 mzpcl34 41401 ntrk0kbimka 42722 isotone1 42731 isotone2 42732 nnfoctbdjlem 45105 isomuspgrlem2d 46433 mgmhmpropd 46489 rnghmmul 46631 2arymaptf1 47240 |
Copyright terms: Public domain | W3C validator |