![]() |
New Foundations Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > NFE Home > Th. List > rexbidv | GIF version |
Description: Formula-building rule for restricted existential quantifier (deduction rule). (Contributed by NM, 20-Nov-1994.) |
Ref | Expression |
---|---|
ralbidv.1 | ⊢ (φ → (ψ ↔ χ)) |
Ref | Expression |
---|---|
rexbidv | ⊢ (φ → (∃x ∈ A ψ ↔ ∃x ∈ A χ)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfv 1619 | . 2 ⊢ Ⅎxφ | |
2 | ralbidv.1 | . 2 ⊢ (φ → (ψ ↔ χ)) | |
3 | 1, 2 | rexbid 2633 | 1 ⊢ (φ → (∃x ∈ A ψ ↔ ∃x ∈ A χ)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 176 ∃wrex 2615 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-3 7 ax-mp 8 ax-gen 1546 ax-5 1557 ax-17 1616 ax-9 1654 ax-8 1675 ax-11 1746 |
This theorem depends on definitions: df-bi 177 df-an 360 df-ex 1542 df-nf 1545 df-rex 2620 |
This theorem is referenced by: rexbii 2639 2rexbidv 2657 rexralbidv 2658 rexeqbi1dv 2816 rexeqbidv 2820 cbvrex2v 2844 rspc2ev 2963 rspc3ev 2965 ceqsrex2v 2974 sbcrexg 3121 uniiunlem 3353 eliun 3973 dfiin2g 4000 pwadjoin 4119 xpkeq2 4199 imakeq1 4224 elimakg 4257 nnc0suc 4412 opklefing 4448 opkltfing 4449 leltfintr 4458 lefinlteq 4463 ncfinraise 4481 ncfinlower 4483 nnpw1ex 4484 tfinprop 4489 tfinltfinlem1 4500 0ceven 4505 evennn 4506 oddnn 4507 evennnul 4508 oddnnul 4509 sucevenodd 4510 sucoddeven 4511 evenodddisj 4516 eventfin 4517 oddtfin 4518 nnadjoin 4520 nnadjoinpw 4521 nnpweq 4523 tfinnn 4534 vfinncvntsp 4549 vfinspsslem1 4550 vfinspss 4551 dfphi2 4569 phi11lem1 4595 0cnelphi 4597 proj1op 4600 proj2op 4601 phialllem1 4616 elima 4754 imaeq1 4937 funcnvuni 5161 fun11iun 5305 fvelrnb 5365 fvelimab 5370 fnasrn 5417 foelrn 5425 foco2 5426 abrexco 5463 funiunfv 5467 f1oiso 5499 f1oiso2 5500 clos1basesuc 5882 qseq2 5975 elqsg 5976 brlecg 6112 ovmuc 6130 ncspw1eu 6159 eqtc 6161 lec0cg 6198 sbth 6206 dflec2 6210 letc 6231 ce0t 6232 ce0lenc1 6239 tcfnex 6244 nncdiv3 6277 |
Copyright terms: Public domain | W3C validator |