|   | Metamath Proof Explorer | < Previous  
      Next > Nearby theorems | |
| Mirrors > Home > MPE Home > Th. List > breq12i | Structured version Visualization version GIF version | ||
| Description: Equality inference for a binary relation. (Contributed by NM, 8-Feb-1996.) (Proof shortened by Eric Schmidt, 4-Apr-2007.) | 
| Ref | Expression | 
|---|---|
| breq1i.1 | ⊢ 𝐴 = 𝐵 | 
| breq12i.2 | ⊢ 𝐶 = 𝐷 | 
| Ref | Expression | 
|---|---|
| breq12i | ⊢ (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐷) | 
| Step | Hyp | Ref | Expression | 
|---|---|---|---|
| 1 | breq1i.1 | . 2 ⊢ 𝐴 = 𝐵 | |
| 2 | breq12i.2 | . 2 ⊢ 𝐶 = 𝐷 | |
| 3 | breq12 5147 | . 2 ⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐷)) | |
| 4 | 1, 2, 3 | mp2an 692 | 1 ⊢ (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐷) | 
| Colors of variables: wff setvar class | 
| Syntax hints: ↔ wb 206 = wceq 1539 class class class wbr 5142 | 
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1794 ax-4 1808 ax-5 1909 ax-6 1966 ax-7 2006 ax-8 2109 ax-9 2117 ax-ext 2707 | 
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3an 1088 df-tru 1542 df-fal 1552 df-ex 1779 df-sb 2064 df-clab 2714 df-cleq 2728 df-clel 2815 df-rab 3436 df-v 3481 df-dif 3953 df-un 3955 df-ss 3967 df-nul 4333 df-if 4525 df-sn 4626 df-pr 4628 df-op 4632 df-br 5143 | 
| This theorem is referenced by: 3brtr3g 5175 3brtr4g 5176 caovord2 7646 domunfican 9362 ltsonq 11010 ltanq 11012 ltmnq 11013 prlem934 11074 prlem936 11088 ltsosr 11135 ltasr 11141 ltneg 11764 leneg 11767 inelr 12257 lt2sqi 14229 le2sqi 14230 nn0le2msqi 14307 2sqreuop 27507 2sqreuopnn 27508 2sqreuoplt 27509 2sqreuopltb 27510 2sqreuopnnlt 27511 2sqreuopnnltb 27512 axlowdimlem6 28963 upgrwlkcompim 29662 clwlkcompbp 29803 mdsldmd1i 32351 fldext2chn 33770 constrextdg2lem 33790 divcnvlin 35734 ditgeq123i 36211 cbvditgvw2 36251 relowlpssretop 37366 2ap1caineq 42147 fsumlessf 45597 climlimsupcex 45789 liminfltlimsupex 45801 liminflelimsupcex 45817 sge0xaddlem2 46454 eubrdm 47053 isgrlim2 47955 iscmgmALT 48145 iscsgrpALT 48147 | 
| Copyright terms: Public domain | W3C validator |