New Foundations Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > NFE Home > Th. List > rexlimdv | GIF version |
Description: Inference from Theorem 19.23 of [Margaris] p. 90 (restricted quantifier version). (Contributed by NM, 14-Nov-2002.) (Proof shortened by Eric Schmidt, 22-Dec-2006.) |
Ref | Expression |
---|---|
rexlimdv.1 | ⊢ (φ → (x ∈ A → (ψ → χ))) |
Ref | Expression |
---|---|
rexlimdv | ⊢ (φ → (∃x ∈ A ψ → χ)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfv 1619 | . 2 ⊢ Ⅎxφ | |
2 | nfv 1619 | . 2 ⊢ Ⅎxχ | |
3 | rexlimdv.1 | . 2 ⊢ (φ → (x ∈ A → (ψ → χ))) | |
4 | 1, 2, 3 | rexlimd 2735 | 1 ⊢ (φ → (∃x ∈ A ψ → χ)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 1710 ∃wrex 2615 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1546 ax-5 1557 ax-17 1616 ax-9 1654 ax-8 1675 ax-6 1729 ax-11 1746 |
This theorem depends on definitions: df-bi 177 df-an 360 df-ex 1542 df-nf 1545 df-ral 2619 df-rex 2620 |
This theorem is referenced by: rexlimdva 2738 rexlimdv3a 2740 rexlimdvw 2741 rexlimdvv 2744 eqpw1uni 4330 nndisjeq 4429 ssfin 4470 nnpw1ex 4484 tfinltfinlem1 4500 sfin112 4529 sfintfin 4532 sfinltfin 4535 funcnvuni 5161 dffo3 5422 nclenn 6249 ncslesuc 6267 |
Copyright terms: Public domain | W3C validator |