![]() |
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 |
---|---|
rmobidv.1 | ⊢ (𝜑 → (𝜓 ↔ 𝜒)) |
Ref | Expression |
---|---|
reubidv | ⊢ (𝜑 → (∃!𝑥 ∈ 𝐴 𝜓 ↔ ∃!𝑥 ∈ 𝐴 𝜒)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | rmobidv.1 | . . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒)) | |
2 | 1 | adantr 481 | . 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒)) |
3 | 2 | reubidva 3391 | 1 ⊢ (𝜑 → (∃!𝑥 ∈ 𝐴 𝜓 ↔ ∃!𝑥 ∈ 𝐴 𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∈ wcel 2106 ∃!wreu 3373 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 |
This theorem depends on definitions: df-bi 206 df-an 397 df-ex 1782 df-mo 2533 df-eu 2562 df-reu 3376 |
This theorem is referenced by: reueqd 3418 sbcreu 3866 oawordeu 8538 xpf1o 9122 dfac2b 10107 creur 12188 creui 12189 divalg 16328 divalg2 16330 lubfval 18285 lubeldm 18288 lubval 18291 glbfval 18298 glbeldm 18301 glbval 18304 joineu 18317 meeteu 18331 dfod2 19396 ustuqtop 23680 addsq2reu 26870 addsqn2reu 26871 addsqrexnreu 26872 addsqnreup 26873 2sqreulem1 26876 2sqreunnlem1 26879 usgredg2vtxeuALT 28344 isfrgr 29378 frcond1 29384 frgr1v 29389 nfrgr2v 29390 frgr3v 29393 3vfriswmgr 29396 n4cyclfrgr 29409 eulplig 29601 riesz4 31180 cnlnadjeu 31194 poimirlem25 36317 poimirlem26 36318 hdmap1eulem 40498 hdmap1eulemOLDN 40499 hdmap14lem6 40549 reuf1odnf 45587 euoreqb 45589 joindm3 47250 meetdm3 47252 |
Copyright terms: Public domain | W3C validator |