New Foundations Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > NFE Home > Th. List > rexlimdva | GIF version |
Description: Inference from Theorem 19.23 of [Margaris] p. 90 (restricted quantifier version). (Contributed by NM, 20-Jan-2007.) |
Ref | Expression |
---|---|
rexlimdva.1 | ⊢ ((φ ∧ x ∈ A) → (ψ → χ)) |
Ref | Expression |
---|---|
rexlimdva | ⊢ (φ → (∃x ∈ A ψ → χ)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | rexlimdva.1 | . . 3 ⊢ ((φ ∧ x ∈ A) → (ψ → χ)) | |
2 | 1 | ex 423 | . 2 ⊢ (φ → (x ∈ A → (ψ → χ))) |
3 | 2 | rexlimdv 2737 | 1 ⊢ (φ → (∃x ∈ A ψ → χ)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 358 ∈ 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: rexlimdvaa 2739 rexlimivv 2743 rexlimdvv 2744 pw1disj 4167 leltfintr 4458 ncfinlower 4483 tfin11 4493 tfinpw1 4494 nnpweq 4523 sfin112 4529 sfindbl 4530 vfinspss 4551 vfinspeqtncv 4553 phi11lem1 4595 foco2 5426 f1elima 5474 ectocld 5991 ncssfin 6151 nntccl 6170 dflec2 6210 leaddc1 6214 leconnnc 6218 tlecg 6230 letc 6231 ce2le 6233 ce0lenc1 6239 nclenn 6249 lemuc1 6253 lecadd2 6266 ncslesuc 6267 nnc3n3p1 6278 nchoicelem17 6305 nchoicelem19 6307 nchoice 6308 dmfrec 6316 fnfreclem3 6319 |
Copyright terms: Public domain | W3C validator |