![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > reubidv | Structured version Visualization version GIF version |
Description: Formula-building rule for restricted existential quantifier (deduction form). (Contributed by NM, 17-Oct-1996.) |
Ref | Expression |
---|---|
reubidv.1 | ⊢ (𝜑 → (𝜓 ↔ 𝜒)) |
Ref | Expression |
---|---|
reubidv | ⊢ (𝜑 → (∃!𝑥 ∈ 𝐴 𝜓 ↔ ∃!𝑥 ∈ 𝐴 𝜒)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | reubidv.1 | . . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒)) | |
2 | 1 | adantr 473 | . 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒)) |
3 | 2 | reubidva 3320 | 1 ⊢ (𝜑 → (∃!𝑥 ∈ 𝐴 𝜓 ↔ ∃!𝑥 ∈ 𝐴 𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 198 ∈ wcel 2051 ∃!wreu 3083 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1759 ax-4 1773 ax-5 1870 |
This theorem depends on definitions: df-bi 199 df-an 388 df-ex 1744 df-mo 2548 df-eu 2585 df-reu 3088 |
This theorem is referenced by: reueqd 3352 sbcreu 3755 oawordeu 7980 xpf1o 8473 dfac2b 9348 creur 11431 creui 11432 divalg 15612 divalg2 15614 lubfval 17458 lubeldm 17461 lubval 17464 glbfval 17471 glbeldm 17474 glbval 17477 joineu 17490 meeteu 17504 dfod2 18464 ustuqtop 22573 addsq2reu 25733 addsqn2reu 25734 addsqrexnreu 25735 addsqnreup 25736 2sqreulem1 25739 2sqreunnlem1 25742 usgredg2vtxeuALT 26722 isfrgr 27807 frcond1 27815 frgr1v 27820 nfrgr2v 27821 frgr3v 27824 3vfriswmgr 27827 n4cyclfrgr 27840 eulplig 28054 riesz4 29637 cnlnadjeu 29651 poimirlem25 34395 poimirlem26 34396 hdmap1eulem 38440 hdmap1eulemOLDN 38441 hdmap14lem6 38491 reuf1odnf 42746 euoreqb 42748 |
Copyright terms: Public domain | W3C validator |