| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > r19.29af | Structured version Visualization version GIF version | ||
| Description: A commonly used pattern based on r19.29 3102. See r19.29a 3147, r19.29an 3143 for a variant when 𝑥 is disjoint from 𝜑. (Contributed by Thierry Arnoux, 29-Nov-2017.) |
| Ref | Expression |
|---|---|
| r19.29af.0 | ⊢ Ⅎ𝑥𝜑 |
| r19.29af.1 | ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝜓) → 𝜒) |
| r19.29af.2 | ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 𝜓) |
| Ref | Expression |
|---|---|
| r19.29af | ⊢ (𝜑 → 𝜒) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | r19.29af.0 | . 2 ⊢ Ⅎ𝑥𝜑 | |
| 2 | nfv 1921 | . 2 ⊢ Ⅎ𝑥𝜒 | |
| 3 | r19.29af.1 | . 2 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝜓) → 𝜒) | |
| 4 | r19.29af.2 | . 2 ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 𝜓) | |
| 5 | 1, 2, 3, 4 | r19.29af2 3247 | 1 ⊢ (𝜑 → 𝜒) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∧ wa 396 Ⅎwnf 1790 ∈ wcel 2119 ∃wrex 3063 |
| 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 1974 ax-7 2015 ax-12 2189 |
| This theorem depends on definitions: df-bi 208 df-an 397 df-ex 1787 df-nf 1791 df-ral 3054 df-rex 3064 |
| This theorem is referenced by: fsnex 7228 neiptopnei 23116 neitr 23164 utopsnneiplem 24231 isucn2 24262 2sqmo 27419 foresf1o 32593 fsumiunle 32922 nsgqusf1olem3 33499 irngnzply1 33884 reff 34032 locfinreflem 34033 ordtconnlem1 34117 esumrnmpt2 34261 esumgect 34283 esum2dlem 34285 esum2d 34286 esumiun 34287 sigapildsys 34355 oms0 34490 eulerpartlemgvv 34569 breprexplema 34823 stoweidlem27 46478 stoweidlem35 46486 |
| Copyright terms: Public domain | W3C validator |