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 3539 | . 2 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (∀𝑥 ∈ 𝐶 ∀𝑦 ∈ 𝐷 𝜑 → 𝜓)) |
4 | 3 | imp 410 | 1 ⊢ (((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) ∧ ∀𝑥 ∈ 𝐶 ∀𝑦 ∈ 𝐷 𝜑) → 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 209 ∧ wa 399 = wceq 1542 ∈ wcel 2114 ∀wral 3054 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1917 ax-6 1975 ax-7 2020 ax-8 2116 ax-9 2124 ax-ext 2711 |
This theorem depends on definitions: df-bi 210 df-an 400 df-tru 1545 df-ex 1787 df-sb 2075 df-clab 2718 df-cleq 2731 df-clel 2812 df-ral 3059 |
This theorem is referenced by: swopo 5463 soisores 7106 soisoi 7107 isocnv 7109 isotr 7115 ovrspc2v 7209 caofrss 7473 caonncan 7478 wunpr 10222 injresinj 13262 seqcaopr2 13511 rlimcn3 15050 o1of2 15073 isprm6 16168 ssc2 17210 pospropd 17873 mhmpropd 18091 grpidssd 18306 grpinvssd 18307 dfgrp3lem 18328 isnsg3 18443 cyccom 18477 symgextf1 18680 efgredlemd 19001 efgredlem 19004 issrngd 19764 domneq0 20202 lindfind 20645 lindsind 20646 mplsubglem 20828 mdetunilem1 21376 mdetunilem3 21378 mdetunilem4 21379 mdetunilem9 21384 decpmatmulsumfsupp 21537 pm2mpf1 21563 pm2mpmhmlem1 21582 t0sep 22088 tsmsxplem2 22918 comet 23279 nrmmetd 23340 tngngp 23420 reconnlem2 23592 iscmet3lem1 24056 iscmet3lem2 24057 dchrisumlem1 26238 pntpbnd1 26335 tgjustc1 26434 tgjustc2 26435 iscgrglt 26473 motcgr 26495 perpneq 26673 foot 26681 f1otrg 26830 axcontlem10 26932 frgr2wwlk1 28279 tleile 30834 orngmul 31092 lindsunlem 31290 mndpluscn 31461 unelros 31722 difelros 31723 inelsros 31729 diffiunisros 31730 cvxsconn 32789 elmrsubrn 33066 frpoins3xpg 33403 ssltsepc 33643 ghomco 35705 sticksstones10 39750 sticksstones12a 39752 fsuppind 39899 mzpcl34 40166 ntrk0kbimka 41236 isotone1 41245 isotone2 41246 nnfoctbdjlem 43576 isomuspgrlem2d 44865 mgmhmpropd 44921 rnghmmul 45040 2arymaptf1 45581 |
Copyright terms: Public domain | W3C validator |