| 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 uniqueness quantifier (deduction form). (Contributed by NM, 17-Oct-1996.) |
| Ref | Expression |
|---|---|
| rmobidv.1 | ⊢ (𝜑 → (𝜓 ↔ 𝜒)) |
| Ref | Expression |
|---|---|
| reubidv | ⊢ (𝜑 → (∃!𝑥 ∈ 𝐴 𝜓 ↔ ∃!𝑥 ∈ 𝐴 𝜒)) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | rmobidv.1 | . . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒)) | |
| 2 | 1 | adantr 480 | . 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒)) |
| 3 | 2 | reubidva 3396 | 1 ⊢ (𝜑 → (∃!𝑥 ∈ 𝐴 𝜓 ↔ ∃!𝑥 ∈ 𝐴 𝜒)) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ↔ wb 206 ∈ wcel 2108 ∃!wreu 3378 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1780 df-mo 2540 df-eu 2569 df-reu 3381 |
| This theorem is referenced by: reueqd 3421 sbcreu 3876 oawordeu 8593 xpf1o 9179 dfac2b 10171 creur 12260 creui 12261 divalg 16440 divalg2 16442 lubfval 18395 lubeldm 18398 lubval 18401 glbfval 18408 glbeldm 18411 glbval 18414 joineu 18427 meeteu 18441 dfod2 19582 ustuqtop 24255 addsq2reu 27484 addsqn2reu 27485 addsqrexnreu 27486 addsqnreup 27487 2sqreulem1 27490 2sqreunnlem1 27493 usgredg2vtxeuALT 29239 isfrgr 30279 frcond1 30285 frgr1v 30290 nfrgr2v 30291 frgr3v 30294 3vfriswmgr 30297 n4cyclfrgr 30310 eulplig 30504 riesz4 32083 cnlnadjeu 32097 poimirlem25 37652 poimirlem26 37653 hdmap1eulem 41824 hdmap1eulemOLDN 41825 hdmap14lem6 41875 reuf1odnf 47119 euoreqb 47121 isuspgrim0 47872 isuspgrimlem 47874 joindm3 48866 meetdm3 48868 upciclem1 48923 upfval2 48934 upfval3 48935 isuplem 48936 |
| Copyright terms: Public domain | W3C validator |