| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > rexbidv2 | Structured version Visualization version GIF version | ||
| Description: Formula-building rule for restricted existential quantifier (deduction form). (Contributed by NM, 22-May-1999.) |
| Ref | Expression |
|---|---|
| rexbidv2.1 | ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝜓) ↔ (𝑥 ∈ 𝐵 ∧ 𝜒))) |
| Ref | Expression |
|---|---|
| rexbidv2 | ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑥 ∈ 𝐵 𝜒)) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | rexbidv2.1 | . . 3 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝜓) ↔ (𝑥 ∈ 𝐵 ∧ 𝜒))) | |
| 2 | 1 | exbidv 1921 | . 2 ⊢ (𝜑 → (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜓) ↔ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝜒))) |
| 3 | df-rex 3071 | . 2 ⊢ (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜓)) | |
| 4 | df-rex 3071 | . 2 ⊢ (∃𝑥 ∈ 𝐵 𝜒 ↔ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝜒)) | |
| 5 | 2, 3, 4 | 3bitr4g 314 | 1 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑥 ∈ 𝐵 𝜒)) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 ∃wex 1779 ∈ wcel 2108 ∃wrex 3070 |
| 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-ex 1780 df-rex 3071 |
| This theorem is referenced by: rexbidva 3177 rexeqbidv 3347 rexssOLD 4061 iuneq12d 5021 exopxfr2 5855 isoini 7358 rexsupp 8207 omabs 8689 elfi2 9454 wemapsolem 9590 ltexpi 10942 rexuz 12940 ncoprmgcdne1b 16687 lpigen 21345 llyi 23482 nllyi 23483 elpi1 25078 ressupprn 32699 xrecex 32902 bnj18eq1 34941 ldual1dim 39167 pmapjat1 39855 mrefg2 42718 islssfg2 43083 fourierdlem71 46192 hoiqssbl 46640 reuxfr1dd 48726 lubeldm2d 48855 glbeldm2d 48856 |
| Copyright terms: Public domain | W3C validator |